seq bugs - running #5467

NikolajBjorner · 2021-08-10T00:51:33Z

Move remaining bugs from #5140

NikolajBjorner · 2021-08-10T00:52:22Z

Commit: ed9341e
OS: Ubuntu 18.04

Refutation soundness issue:

[644] % z3release model_validate=true small.smt2
sat
[645] % z3-4.8.10 model_validate=true rewriter.pull_cheap_ite=true smt.arith.bprop_on_pivoted_rows=false rewriter.flat=false small.smt2
sat
[646] % cvc5 -q --strings-exp small.smt2
sat
[647] % z3release model_validate=true rewriter.pull_cheap_ite=true smt.arith.bprop_on_pivoted_rows=false rewriter.flat=false small.smt2
unsat
[648] % cat small.smt2
(declare-fun a () String)
(assert (str.contains (str.substr a (+ (str.indexof a "C" 0) 1) (- (str.len a) (+ (str.indexof a "C" 0) 1))) "C"))
(assert (= (ite (= (str.at a (- (str.len a) 1)) "A") 1 0) (+ (str.indexof a "C" 0) 1)))
(assert (not (str.contains (str.substr a (div 1 (ite (= (str.at a 0) "A") 1 0)) (- (+ (str.indexof a "C" 0) 1) (- (str.len a) 1 (ite (= (str.at a 0) "AA") 1 0) (ite (= (str.at a 0) "A") 1 0)))) "B")))
(assert (>= (str.indexof a "C" 0) (ite (= (str.at a 0) "B") 1 0)))
(check-sat)
[649] %

NikolajBjorner · 2021-08-10T00:53:12Z

Commit: d5c6abe
OS: Ubuntu 18.04

Refutation soundness issue on an incremental instance:

[674] % cvc5 -q -i --dump-models small.smt2
sat
(
(define-fun a () String "")
)
sat
(
(define-fun a () String "")
)
[675] % z3-4.8.10 small.smt2
sat
unsat
[676] % z3release small.smt2
sat
unsat
[677] % 
[677] % cat small.smt2
(declare-fun a () String)
(check-sat
 (not
  (str.in_re (str.++ "auzb" a)
   (re.++
    (re.*
     (re.union (re.opt (str.to_re "b"))
      (re.union
       (re.++ (str.to_re "b")
        (re.union (str.to_re "zb") (str.to_re "z") (str.to_re "a")))
       (str.to_re a))))
    (str.to_re "b")))))
(assert (<= (str.len a) 0))
(check-sat)
[678] %

NikolajBjorner · 2021-08-10T00:53:36Z

Commit: 32beb91
OS: Ubuntun 18.04

Refutation unsoundness:

[588] % z3release small.smt2
unsat
[589] % z3-4.8.11 small.smt2
unsat
[590] % z3-4.8.10 small.smt2
unsat
[591] % z3-4.8.8 small.smt2
sat
[592] % cvc4 -q --strings-exp small.smt2
sat
[593] % cat small.smt2
(declare-fun s () String)
(declare-fun i () Int)
(assert (str.contains s "aaaaaaa"))
(assert (= (str.len s) i))
(assert (= (not (= (str.indexof s "aaaaaaa" (- (+ i i) 30)) (- 1))) (str.contains s "bbbbbbbbbbaaaaaaab") (> i 0)))
(check-sat)
[594] %

rainoftime · 2021-08-12T08:17:46Z

an instance involving nth

(declare-fun z () (Seq Bool))
(assert (not (seq.nth (as seq.empty (Seq Bool)) 0)))
(assert (seq.nth (seq.extract z 1 (- (seq.len z) 1)) 0))
(check-sat)

(set-option :rewriter.eq2ineq true)
(declare-fun z () Int)
(declare-fun b () (Seq Int))
(declare-fun y () Int)
(declare-fun a () (Seq Int))
(declare-fun x () Int)
(assert (and (= 1 z) (distinct (seq.nth b x) (seq.nth a z)) (= (seq.nth b y) (seq.nth b 1))))
(assert (> x 0))
(assert (> z 0))
(check-sat)

boboben1 · 2021-09-02T23:41:28Z

Python, but SeqSort(BitVecSort(8)).is_string() is false in 4.8.12.

This has practical effect in a simple case like this:

from z3 import *

s = Solver()
a = String("a")
b = BitVec('b', 8)

s.add(And(SubString(a, 0, 1) == Unit(b), b == 97))

if sat == s.check():
    model = s.model()

    print(model[a])

This will result in a sort mismatch in 4.8.12. It works in 4.8.10.

NikolajBjorner · 2021-09-02T23:49:46Z

It switched to Unicode from Ascii. Character sorts, including Unicode is a separate sort different from BitVec 8.
There are functions for creating character sorts in the python bindings. The String sort is already a sequence sort of unicode characters.

zhendongsu · 2021-09-11T09:30:59Z

Refutation unsoundness (regression from 4.8.12):

[547] % z3-4.8.9 small.smt2
sat
[548] % z3-4.8.10 small.smt2
sat
[549] % z3-4.8.11 small.smt2
sat
[550] % z3-4.8.12 small.smt2
sat
[551] % z3release small.smt2
unsat
[552] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.++ (re.opt (str.to_re "A")) (str.to_re "A") (str.to_re "A") (str.to_re "A"))))
(check-sat)
[553] %

@veanes: this now triggers an assertion violation

zhendongsu · 2021-09-11T09:57:47Z

Solution unsoundness:

[592] % cvc5 -q --strings-exp small.smt2
unsat
[593] % z3-4.8.12 small.smt2
unknown
[594] % z3release model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
[595] % cat small.smt2
(declare-fun a () String)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (str.in_re (str.++ a "A") (re.* (str.to_re (str.substr "B" b c)))))
(check-sat)
[596] %

zhendongsu · 2021-09-11T10:13:26Z

Invalid model (likely related to #5467 (comment)):

[666] % z3-4.8.12 small.smt2
unknown
(error "line 5 column 10: model is not available")
[667] % cvc4 -q --strings-exp --produce-models small.smt2
sat
(
(define-fun a () Int 2)
(define-fun b () String "AAA")
)
[668] % z3release model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
(
  (define-fun b () String
    "BB")
  (define-fun a () Int
    21242)
)
[669] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () String)
(assert (str.in_re (str.++ b "A") (re.* (str.to_re (str.substr b 1 a)))))
(check-sat)
(get-model)
[670] %

zhendongsu · 2021-09-11T12:14:36Z

Invalid model (regression from 4.8.12; possibly related to #5467 (comment)):

[763] % z3-4.8.12 model_validate=true small.smt2
sat
(
  (define-fun a () String
    "B")
  (define-fun b () String
    "A")
)
[764] % z3release model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(
  (define-fun b () String
    "A")
  (define-fun a () String
    "")
)
[765] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (= b "A"))
(assert (not (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B") (str.to_re "A") (str.to_re "A")))))
(check-sat)
(get-model)
[766] %

@veanes: same assertion violation

rainoftime · 2021-09-13T12:06:38Z

at 34f878f

(declare-fun str6 () String)
(assert (str.in_re str6 (re.++ re.all (str.to_re "qk") (str.to_re "C"))))

ASSERTION VIOLATION
File: ../src/ast/rewriter/seq_rewriter.cpp
Line: 3799
re().min_length(tl) == re().max_length(tl)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

zhendongsu · 2021-09-13T14:46:19Z

at 34f878f

(declare-fun str6 () String)
(assert (str.in_re str6 (re.++ re.all (str.to_re "qk") (str.to_re "C"))))

ASSERTION VIOLATION
File: ../src/ast/rewriter/seq_rewriter.cpp
Line: 3799
re().min_length(tl) == re().max_length(tl)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Interestingly, the test from #5467 (comment) also triggers this assertion violation on the debug build:

[523] % z3debug small.smt2 
ASSERTION VIOLATION
File: ../src/ast/rewriter/seq_rewriter.cpp
Line: 3799
re().min_length(tl) == re().max_length(tl)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[524] % cat small.smt2 
(declare-fun a () String)
(assert (str.in_re a (re.++ (re.opt (str.to_re "A")) (str.to_re "A") (str.to_re "A") (str.to_re "A"))))
(check-sat)
[525] %

zhendongsu · 2021-09-13T20:29:59Z

Refutation unsoundness (regression from 4.8.10):

[600] % z3-4.8.10 small.smt2
sat
[601] % cvc4 --strings-exp -q small.smt2
sat
[602] % z3-4.8.11 small.smt2
unsat
[603] % z3-4.8.12 small.smt2
unsat
[604] % z3release small.smt2
unsat
[605] % cat small.smt2
(declare-fun a () String)
(declare-fun b () Int)
(assert (str.contains a "AAAAAAAAABBBBBBBC"))
(assert (= (str.len a) (- b (abs (str.len a)))))
(assert (not (= (str.indexof a "BBBBBBB" (- b 30)) (- 1))))
(check-sat)
[606] %

zhendongsu · 2021-09-14T08:06:05Z

Solution unsoundness:

[556] % cvc5 -q --strings-exp small.smt2
unsat
[557] % z3release model_validate=true small.smt2
sat
(error "line 3 column 10: an invalid model was generated")
[558] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.++ a "AA") (re.++ (re.* (str.to_re "B")) (str.to_re (str.substr (str.++ "B" a) (str.len a) (str.len a))))))
(check-sat)
[559] %

@veanes - this is so far the only remining regex bug in this thread.

zhendongsu · 2021-10-01T12:01:23Z

Solution unsoundness:

[633] % cvc5 -q --strings-exp small.smt2
unsat
(error "Cannot get model unless model generation is enabled (try --produce-models)")
[634] % z3release model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
(
  (define-fun b () String
    "A")
  (define-fun a () String
    "AA")
)
[635] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re a (re.* (str.to_re "A"))))
(assert (str.in_re (str.++ a "B") (re.* (str.to_re (str.substr b 0 (str.len a))))))
(check-sat)
(get-model)
[636] %

zhendongsu · 2021-10-08T08:54:07Z

Refutation unsoundness:

[520] % z3release small.smt2
sat
[521] % z3release rewriter.eq2ineq=true small.smt2
unsat
[522] % cat small.smt2
(declare-fun a () String)
(declare-fun x () Int)
(assert (str.contains a "Hello and goodbye!"))
(assert (= (str.len a) x))
(assert (not (= (str.indexof a "goodbye" (- (+ x x) 30)) (- 1))))
(check-sat)
[523] %

NB: This has to be a duplicate. There are 2 other bugs with similar structure on this thread.

NikolajBjorner · 2021-10-12T18:13:36Z

remaining moved to #5591

NikolajBjorner mentioned this issue Aug 10, 2021

Invalid model in string formula #5140

Closed

NikolajBjorner assigned NikolajBjorner and veanes Aug 10, 2021

NikolajBjorner added the string label Aug 10, 2021

NikolajBjorner closed this as completed Sep 2, 2021

NikolajBjorner reopened this Sep 2, 2021

mrkmarron mentioned this issue Sep 21, 2021

Refutation Unsoundness -- Regex #5562

Closed

NikolajBjorner added a commit that referenced this issue Oct 12, 2021

#5467

52032b9

NikolajBjorner closed this as completed Oct 12, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

seq bugs - running #5467

seq bugs - running #5467

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

rainoftime commented Aug 12, 2021 •

edited

Loading

boboben1 commented Sep 2, 2021

NikolajBjorner commented Sep 2, 2021

zhendongsu commented Sep 11, 2021 •

edited by NikolajBjorner

Loading

zhendongsu commented Sep 11, 2021

zhendongsu commented Sep 11, 2021

zhendongsu commented Sep 11, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Sep 13, 2021

zhendongsu commented Sep 13, 2021

zhendongsu commented Sep 13, 2021

zhendongsu commented Sep 14, 2021 •

edited by NikolajBjorner

Loading

zhendongsu commented Oct 1, 2021

zhendongsu commented Oct 8, 2021 •

edited by NikolajBjorner

Loading

NikolajBjorner commented Oct 12, 2021

seq bugs - running #5467

seq bugs - running #5467

Comments

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

NikolajBjorner commented Aug 10, 2021

rainoftime commented Aug 12, 2021 • edited Loading

boboben1 commented Sep 2, 2021

NikolajBjorner commented Sep 2, 2021

zhendongsu commented Sep 11, 2021 • edited by NikolajBjorner Loading

zhendongsu commented Sep 11, 2021

zhendongsu commented Sep 11, 2021

zhendongsu commented Sep 11, 2021 • edited by NikolajBjorner Loading

rainoftime commented Sep 13, 2021

zhendongsu commented Sep 13, 2021

zhendongsu commented Sep 13, 2021

zhendongsu commented Sep 14, 2021 • edited by NikolajBjorner Loading

zhendongsu commented Oct 1, 2021

zhendongsu commented Oct 8, 2021 • edited by NikolajBjorner Loading

NikolajBjorner commented Oct 12, 2021

rainoftime commented Aug 12, 2021 •

edited

Loading

zhendongsu commented Sep 11, 2021 •

edited by NikolajBjorner

Loading

zhendongsu commented Sep 11, 2021 •

edited by NikolajBjorner

Loading

zhendongsu commented Sep 14, 2021 •

edited by NikolajBjorner

Loading

zhendongsu commented Oct 8, 2021 •

edited by NikolajBjorner

Loading