Z3 invalid model on QF_S formula

[muchang]

Hi, For this formula:

(declare-fun a () String)
(assert (let ((b (str.substr a 10 (str.len a))))
         (let ((c (str.substr a 0 (- (str.len b) (+ (str.indexof b "z" 0) 1)))))
          (and (= (str.len c) 0) (str.prefixof "yyyz" a) (str.contains a "z")))))
(check-sat)
(get-model)

Z3 gives an invalid model:

(model 
  (define-fun a () String
    "yyyz\x00\x00\x00\x00\x00\x00zz")
)

if I feed this model to the formula, Z3 reports unsat.

OS: Ubuntu 18.04 Commit: 1aea0d2

[mtrberzi]

To clarify, are you running with smt.string_solver=z3str3 or a different/no setting?

[NikolajBjorner]

this is by seq solver, not z3str3

[NikolajBjorner]

C:\z3\build>z3 3062.smt2  model_validate=true /st
sat
(error "line 5 column 10: an invalid model was generated")
(model
  (define-fun a () String
    "yyyz\x00\x00\x00\x00\x00\x00zz")
)
(:added-eqs            3268
 :arith-add-rows       549
 :arith-assert-diseq   50
 :arith-assert-lower   341
 :arith-assert-upper   209
 :arith-bound-prop     34
 :arith-conflicts      13
 :arith-eq-adapter     156
 :arith-fixed-eqs      122
 :arith-offset-eqs     72
 :arith-pivots         66
 :binary-propagations  165
 :bv-bit2core          2214
 :bv-conflicts         1
 :bv->core-eq          259
 :conflicts            25
 :decisions            1008
 :del-clause           119
 :final-checks         52
 :interface-eqs        10
 :max-memory           4.54
 :memory               3.02
 :minimized-lits       1
 :mk-bool-var          2779
 :mk-clause            252
 :num-allocs           3690723
 :num-checks           2
 :propagations         299
 :rlimit-count         42614
 :seq-add-axiom        700
 :seq-branch           12
 :seq-fixed-length     18
 :seq-length-coherence 9
 :seq-num-reductions   326
 :time                 0.30
 :total-time           0.34)

The statistics show that it uses the seq solver.

[muchang]

From https://github.com/Z3Prover/z3/issues/3105 Hi, For this formula:

(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (distinct (str.substr a 3 (str.len b)) ""))
(assert (distinct
         (ite (= (str.len (str.substr (str.replace a b "") 0 (- (str.len c)))) 1) 0 2)
         (ite (= (str.at (str.replace a b "") 2) "") 1 2)))
(check-sat)
(get-model)

Z3 gives an invalid model:

(model 
  (define-fun b () String
    "\x00")
  (define-fun a () String
    "\x00\x00\x00\x00\x00")
  (define-fun c () String
    "\x00")
)

if I feed this model to the formula, Z3 reports unsat.

OS: Ubuntu 18.04 Commit: ad6062c

[NikolajBjorner]

2937

Consider the following formula.

(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.prefixof a (str.substr b 20 2)) (str.prefixof a (str.at b 7))))
(check-sat)
(get-model)

Z3 gives the following incorrect model.

(model 
  (define-fun b () String
    "\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00")
  (define-fun a () String
    "\x80")
)

OS: Ubuntu 18.04 Revision: 06173aa

[NikolajBjorner]

From #2896

This also reproduces bug

(declare-fun s () String)
(assert (not (str.contains (str.substr s 2 (str.len s)) "c")))
(assert (str.contains s "b"))
(assert (str.prefixof "aa" s))
(assert (str.contains s "c"))
(check-sat)
(get-model)