Zhendong Su

Another instance: ``` [605] % z3release model_validate=true small.smt2 sat sat sat sat sat (error "line 14 column 10: an invalid model was generated") [606] % cat small.smt2 (declare-const a Bool)...

``` [539] % z3release model_validate=true small.smt2 sat sat sat sat sat [540] % z3release model_validate=true smt.threads=2 small.smt2 sat sat sat sat sat (error "line 10 column 10: an invalid model...

A solution unsoundness instance: ``` [515] % z3release small.smt2 sat sat sat sat sat unsat unsat unsat [516] % z3release smt.threads=2 small.smt2 sat sat sat sat sat unsat unsat sat...

Nikolaj (@NikolajBjorner), looks like the following two instances still reproduce: - https://github.com/Z3Prover/z3/issues/6346#issuecomment-1250763728 - https://github.com/Z3Prover/z3/issues/6346#issuecomment-1256913930

``` [604] % z3release model_validate=true small.smt2 sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat (error "line 46 column 10: an invalid...

``` [522] % z3release model_validate=true small.smt2 sat sat sat sat (error "line 10 column 10: an invalid model was generated") [523] % cat small.smt2 (declare-fun x () Bool) (declare-fun y...

Both Z3 and CVC4 report sat. Below is the model from Z3: ``` (model (define-fun b () Int (- 2)) (define-fun a () String "\x00\x00\x00") ) ```

Adding a few cases (there seem to be quite many): ``` [514] % z3release small.smt2 unsat [515] % z3release smt.string_solver=z3str3 small.smt2 sat [516] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 sat (error...

``` [522] % z3release small.smt2 unsat [523] % z3release smt.string_solver=z3str3 small.smt2 sat [524] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 sat (error "line 3 column 10: an invalid model was generated") [525]...

``` [533] % z3release model_validate=true small.smt2 sat [534] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 sat (error "line 3 column 10: an invalid model was generated") [535] % cat small.smt2 (declare-fun a...