Consolidated bugs in string logics

[wintered]

Refutation soundness bug on Z3 trunk. z3-4.8.8 returns the correct result which is sat.

[581] % z3-4.8.8 small.smt2
sat
[582] % z3release small.smt2
unsat
[583] % 
[583] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (= (str.substr a 0 (str.len b)) "B"))
(assert (= (str.replace a b "") (str.++ "A" b)))
(check-sat)
[584] %

Commit: 395a304
OS: Ubuntu 18.04

NB: Fixed

[wintered]

Another, possibly different soundness bug.

[522] % z3-4.8.8 small.smt2
sat
[523] % z3release small.smt2
unsat
[524] % 
[524] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(assert (= (str.substr a 0 (str.len d)) "AAA"))
(assert (not (str.contains c "A")))
(assert (= (str.substr a 0 (str.len b)) "A"))
(assert (= (str.indexof c "B" 0) 0))
(check-sat)
[525] %

OS: Ubuntu 18.04
Commit: 3b11493

NB: Fixed

[zhendongsu]

An instance for solution unsoundness for the qe2 tactic (regression from z3-4.8.8):

[606] % z3-4.8.8 small.smt2
unsat
unsat
[607] % z3release small.smt2
sat
unsat
[608] % 
[608] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in.re (str.++ a "z" b) (re.* (str.to.re "b"))))
(assert (str.in.re (str.++ a "z" b) (re.+ (re.+ (str.to.re "b")))))
(assert (str.in.re (str.++ a "z" b) (re.* (str.to.re "zaa"))))
(assert (str.in.re (str.++ a "z" b) (re.opt (str.to.re "z"))))
(assert (str.in.re a (re.opt (re.range "a" "u"))))
(check-sat-using qe2)
(check-sat)
[609] % 

OS: Ubuntu 18.04
Commit: 274323b

NB: stale now with different str.in_re solver

[zhendongsu]

Another refutation unsoundness instance (regression from z3-4.8.8 and likely related to the first two instances in this thread):

[591] % z3-4.8.8 small.smt2
sat
[592] % z3release small.smt2
unsat
[593] % 
[593] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (= b (str.substr a 1 (- (str.len a) 1))))
(assert (str.contains (str.substr b 0 (- (str.len b) 1)) "A"))
(assert (= (str.at b (- (str.len b) 1)) "B"))
(assert (distinct (str.at b 0) "A"))
(check-sat)
[594] % 

OS: Ubuntu 18.04
Commit: 274323b

NB: Fixed

[zhendongsu]

A refutation unsoundness instance with the ctx-solver-simplify tactic:

[540] % z3-4.8.8 small.smt2
unknown
sat
[541] % z3release small.smt2
unsat
sat
[542] % cat small.smt2
(declare-fun b () String)
(assert (not (str.contains b "A")))
(assert (<= 0 (str.indexof b "B") 0))
(check-sat-using ctx-solver-simplify)
(check-sat)
[543] % 

OS: Ubuntu 18.04
Commit: 274323b

NB: Fixed

[zhendongsu]

A refutation unsoundness instance when using smt.threads=2:

[625] % z3release small.smt2
sat
[626] % z3release smt.threads=2 small.smt2
unsat
[627] % 
[627] % cat small.smt2
(declare-fun a () String)
(declare-fun x () String)
(assert (str.in_re x (re.++ (str.to_re "baa") (re.+ (str.to_re "a")) (re.* (str.to_re "c")))))
(assert
 (xor (str.in_re x (re.union (str.to_re "baa") (re.+ (str.to_re "a")) (re.comp (str.to_re "a"))))
  (str.in_re x (re.* (str.to_re "c")))
  (not (str.in_re x (re.union (re.+ (str.to_re "a")) (str.to_re "a"))))
  (str.in_re a (re.++ re.all re.all (re.comp re.allchar) re.all))
  (str.in_re a re.allchar)))
(check-sat)
[628] % 

OS: Ubuntu 18.04
Commit: 02f34ea

[NikolajBjorner]

The bugs that use "str.in_re" should go away when we switch to a different backend for regular expressions.
The cause is known but will not be fixed in the current way they are solved.

[zhendongsu]

The bugs that use "str.in_re" should go away when we switch to a different backend for regular expressions.
The cause is known but will not be fixed in the current way they are solved.

Okay, Nikolaj, for now, we will not report additional bugs involving "str.in_re" then; thanks.

[zhendongsu]

Another refutation unsoundness instance (regression from z3-4.8.8 and likely related to some of the earlier instances in this thread, but this instance does not involve str.contains nor str.replace):

[578] % z3-4.8.8 small.smt2
sat
[579] % z3release small.smt2
unsat
[580] % 
[580] % cat small.smt2
(set-logic QF_S)
(declare-fun a () String)
(assert (= (str.substr a 0 (str.indexof (str.substr a 0 (- (str.len a) 1)) "A" 0)) "B"))
(assert (= (str.at a (- (str.len a) 1)) "C"))
(check-sat)
[581] % 

OS: Ubuntu 18.04
Commit: 6ced699

NB: Fixed

[zhendongsu]

A refutation unsoundness instance for which arith.solver=2 correctly answers sat, while arith.solver=6 gives the incorrect unsat:

[583] % z3release smt.arith.solver=2 small.smt2
sat
[584] % z3release smt.arith.solver=6 small.smt2
unsat
[585] % cat small.smt2
(set-logic QF_SLIA)
(declare-fun a () String)
(assert (str.contains (str.substr a 0 (- (str.len a) 1)) "A"))
(assert (= (ite (= (str.at a 0) "B") 1 0) (ite (= (str.at a 0) "A") 1 0) 0))
(assert (= (str.at a (- (str.len a) 1)) "B"))
(check-sat)
[586] % 

OS: Ubuntu 18.04
Commit: 64f1a75

NB: Fixed

[zhendongsu]

A refutation unsoundness instance for which arith.solver=6 correctly answers sat, while arith.solver=2 gives the incorrect unsat:

[727] % z3release small.smt2
sat
[728] % z3release smt.arith.solver=6 rewriter.flat=false small.smt2
sat
[729] % z3release smt.arith.solver=2 rewriter.flat=false small.smt2
unsat
[730] % 
[730] % cat small.smt2
(declare-fun a () String)
(assert
 (and (str.contains (str.substr a 0 (- (str.len a) 1)) " ")
  (distinct (str.len (str.substr a 0 (- (str.len a) 1))) 0)
  (distinct (str.at (str.substr a 0 1) (- (str.len (str.substr a 0 (- (- (str.len a) 1)))) 1)) "A")
  (distinct (str.at (str.substr a 0 (- (- (str.len a) 1))) 0) "B")
  (distinct (str.at (str.substr a 0 (- (- (str.len a) 1))) 0) "\n")
  (= (str.at a (- (str.len a) 1)) "\n") (distinct (str.at a 0) " ")))
(check-sat)
[731] % 

OS: Ubuntu 18.04
Commit: 23e6adc

NB: Fixed

[zhendongsu]

An invalid model instance for arith.solver=6, but not arith.solver=2:

[600] % z3release model_validate=true smt.arith.solver=2 small.smt2 
sat
(model 
  (define-fun s () String
    "A\x00\x00")
)
[601] % z3release model_validate=true smt.arith.solver=6 small.smt2 
sat
(error "line 8 column 10: an invalid model was generated")
(model 
  (define-fun s () String
    "A")
)
[602] % 
[602] % cat small.smt2
(declare-fun s () String)
(assert (>= (- (str.len s) (str.indexof s "A") 1) 0))
(assert (>= (str.len (str.substr s (+ (str.indexof s "A") 1) (- (str.len s) (str.indexof s "A") 1))) 1))
(assert (>= (str.len (str.substr s (+ (str.indexof s "A") 1) (- (str.len s) 1))) 1))
(assert (>= (+ (str.indexof s "A" 30) 1) 0))
(assert (>= (str.len (str.substr s (+ (str.indexof s "A" 20) 1) (- (str.len s) (str.indexof s "A") 1))) 1))
(assert (>= (str.indexof s "A") 0))
(check-sat)
(get-model)
[603] % 

OS: Ubuntu 18.04
Commit: d3ae401

NB: stopped reproducing

[zhendongsu]

An instance that causes z3 to segfault:

[584] % z3release small.smt2
Segmentation fault
[585] % 
[585] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.++ a "z" b) (re.+ (re.+ (str.to_re "b")))))
(assert (str.in_re (str.++ a "z" b) (re.* (re.union (str.to_re "b") (str.to_re "a")))))
(assert (str.in_re (str.++ a "z" b) (re.* (re.union (str.to_re "z") (str.to_re "b")))))
(assert (str.in_re (str.++ a "z" b) (re.* (re.++ (re.* (str.to_re "z")) (str.to_re "b")))))
(check-sat-using (then ctx-solver-simplify))
[586] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==10921==ERROR: AddressSanitizer: stack-overflow on address 0x7fff5eb3ee78 (pc 0x7f7d125bf576 bp 0x7fff5eb3f700 sp 0x7fff5eb3ee80 T0)
    #0 0x7f7d125bf575  (/usr/lib/x86_64-linux-gnu/libasan.so.4+0x51575)
    #1 0x5597fddc23fa in internal_symbol_tables::get_str(char const*) ../src/util/symbol.cpp:94
    #2 0x5597fddc23fa in symbol::symbol(char const*) ../src/util/symbol.cpp:123
    #3 0x5597fc931f9a in ast_manager::mk_family_id(char const*) ../src/ast/ast.h:1608
    #4 0x5597fc931f9a in seq_util::seq_util(ast_manager&) ../src/ast/seq_decl_plugin.h:483
    #5 0x5597fc931f9a in sym_expr_boolean_algebra::mk_and(sym_expr*, sym_expr*) ../src/ast/rewriter/seq_rewriter.cpp:104
    #6 0x5597fc9471e9 in symbolic_automata<sym_expr, sym_expr_manager>::generate_min_terms_rec(vector<obj_ref<sym_expr, sym_expr_manager>, true, unsigned int>&, vector<std::pair<vector<bool, true, unsigned int>, obj_ref<sym_expr, sym_expr_manager> >, true, unsigned int>&, unsigned int, vector<bool, true, unsigned int>&, obj_ref<sym_expr, sym_expr_manager>&) ../src/math/automata/symbolic_automata.h:135
    #7 0x5597fc94729d in symbolic_automata<sym_expr, sym_expr_manager>::generate_min_terms_rec(vector<obj_ref<sym_expr, sym_expr_manager>, true, unsigned int>&, vector<std::pair<vector<bool, true, unsigned int>, obj_ref<sym_expr, sym_expr_manager> >, true, unsigned int>&, unsigned int, vector<bool, true, unsigned int>&, obj_ref<sym_expr, sym_expr_manager>&) ../src/math/automata/symbolic_automata.h:136
    #8 0x5597fc94729d in symbolic_automata<sym_expr, sym_expr_manager>::generate_min_terms_rec(vector<obj_ref<sym_expr, sym_expr_manager>, true, unsigned int>&, vector<std::pair<vector<bool, true, unsigned int>, obj_ref<sym_expr, sym_expr_manager> >, true, unsigned int>&, unsigned int, vector<bool, true, unsigned int>&, obj_ref<sym_expr, sym_expr_manager>&) ../src/math/automata/symbolic_automata.h:136
...
SUMMARY: AddressSanitizer: stack-overflow (/usr/lib/x86_64-linux-gnu/libasan.so.4+0x51575) 
==10921==ABORTING

OS: Ubuntu 18.04
Commit: d3ae401

NB; stale

[zhendongsu]

A refutation unsoundness instance with the ctx-solver-simplify tactic:

[619] % z3release small.smt2
unsat
sat
[620] % cat small.smt2
(declare-fun a () String)
(assert (= (str.len (str.substr a 0 (str.indexof a "a"))) 0))
(assert (str.contains a "a"))
(assert (not (str.contains a "b")))
(check-sat-using ctx-solver-simplify)
(check-sat)
[621] % 

OS: Ubuntu 18.04
Commit: 2ef57d7

NB: Fixed

[NikolajBjorner]

Current status:

• str.in_re bugs will be dealt with separately.
• refutation soundness bugs seem to all be traced to the same root cause and are no longer showing up.
• invalid model generation remains. There are some other github issues that relate to invalid models being produced.