Invalid model in string formula

[jiwonparc]

commit: c629f09

$ z3release model_validate=true small.smt2
sat
(error "line 13 column 10: an invalid model was generated")
$ cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
 (re.++
  (re.diff
  (re.++ (re.* (re.union (str.to_re "a") (str.to_re "b"))) (str.to_re "b"))
  (re.++
   (re.inter
   (re.++ (re.++ (re.* (re.union (str.to_re "a") (str.to_re "b"))) (str.to_re "b")) (str.to_re a))
   (re.++ (re.* (re.union (str.to_re "a") (str.to_re "b")))))
   (str.to_re "a")))
  (str.to_re (ite (str.in_re a (re.union (str.to_re "b"))) "b" "a""b")))))
(check-sat)

[jiwonparc]

commit: c629f09
simpler case

$ z3release model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
(
 (define-fun b () String
  "")
 (define-fun a () String
  "z")
)
$ z3-4.8.10 model_validate=true small.smt2
sat
(
 (define-fun b () String
  "")
 (define-fun a () String
  "b")
)
$ cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re a
     (re.diff (re.union (re.* (str.to_re "b")) (str.to_re "z"))
     (re.++ (re.* (str.to_re "z")) (str.to_re b)))))
(assert (= 0 (str.len b)))
(check-sat)
(get-model)

[NikolajBjorner]

@veanes @cdstanford : maybe connected with symbolic regexes. (str.to_re b) is symbolic.
Could you check?

[jiwonparc]

commit: 1fc9a7b

$ z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
$ z3-4.8.10 model_validate=true small.smt2
sat
$ cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
 (re.++
  (str.to_re
  (ite (str.in_re a (re.++ (str.to_re "\u\u\u\u\u") (re.* re.allchar))) a "\u\u\u\u\u"))
  (re.* re.allchar))))
(check-sat)

[cdstanford]

These are very interesting non-ground test cases. I verified the buggy behavior for the 5 examples on the most recent commit (1fc9a7b)

A slightly simpler version of the second example:

(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re a
    (re.inter
        (re.union (str.to_re "0") (str.to_re "1"))
        (re.comp (re.++ (re.* (str.to_re "1")) (str.to_re b)))
    )
))
(assert (= 0 (str.len b)))
(check-sat)
(get-model)

The example behaves correctly if (assert (= 0 (str.len b))) is replaced by the equivalent (assert (= b "")), suggesting something to do with the interaction between the solver and length constraints.
But the fact these bugs are only present at model validation stage is a bit surprising.
I haven't investigated the regex solver traces yet.

The third example seems to rely on the \u\u\u\u\u input, does not fail with a smaller (less than 5) sequence of \u or if \u is replaced by 0. So possibly something to do with unicode and string encoding, and thus not as worth investigating first (i.e. we should revisit after we figure out the problem in the first and second examples).

[cdstanford]

-dbg:seq_regex throws assertion violations because our code which checks derivative normal form doesn't deal with non-ground regexes.

Output of -tr:seq_regex:

-------- [seq_regex] propagate_in_re ../src/smt/seq_regex.cpp:94 ---------
propagate in RE: 0 (let ((a!1 (re.union (re.* (str.to_re (seq.unit (_ Char 98))))
                     (str.to_re (seq.unit (_ Char 122)))))
      (a!2 (re.++ (re.* (str.to_re (seq.unit (_ Char 122)))) (str.to_re b))))
  (str.in_re a (re.inter a!1 (re.comp a!2))))
------------------------------------------------
-------- [seq_regex] propagate_accept ../src/smt/seq_regex.cpp:270 ---------
propagate accept: (let ((a!1 (re.union (re.* (str.to_re (seq.unit (_ Char 98))))
                     (str.to_re (seq.unit (_ Char 122)))))
      (a!2 (re.++ (re.* (str.to_re (seq.unit (_ Char 122)))) (str.to_re b))))
  (aut.accept a 0 (re.inter a!1 (re.comp a!2))))
------------------------------------------------
nullable: (let ((a!1 (re.union (re.* (str.to_re (seq.unit (_ Char 98))))
                     (str.to_re (seq.unit (_ Char 122)))))
      (a!2 (re.++ (re.* (str.to_re (seq.unit (_ Char 122)))) (str.to_re b))))
  (re.inter a!1 (re.comp a!2)))
nullable result: (not (= "" b))
Warning: is_nullable did not simplify to true or false
derivative((seq.nth_i a 0)): (let ((a!1 (re.union (re.* (str.to_re (seq.unit (_ Char 98))))
                     (str.to_re (seq.unit (_ Char 122)))))
      (a!2 (re.++ (re.* (str.to_re (seq.unit (_ Char 122)))) (str.to_re b))))
  (re.inter a!1 (re.comp a!2)))
derivative result: (let ((a!1 (re.inter (re.* (str.to_re (seq.unit (_ Char 98))))
                     (re.comp (re.derivative (seq.nth_i a 0) (str.to_re b)))))
      (a!3 (re.++ (re.* (str.to_re (seq.unit (_ Char 122)))) (str.to_re b)))
      (a!4 (re.inter (re.comp (re.derivative (seq.nth_i a 0) (str.to_re b)))
                     (str.to_re ""))))
(let ((a!2 (ite (char.<= (seq.nth_i a 0) (_ Char 98))
                (ite (char.<= (seq.nth_i a 0) (_ Char 97)) re.none a!1)
                re.none)))
  (ite (char.<= (seq.nth_i a 0) (_ Char 122))
       (ite (char.<= (seq.nth_i a 0) (_ Char 121))
            a!2
            (re.inter (re.comp a!3) a!4))
       re.none)))
-------- [seq_regex] propagate_accept ../src/smt/seq_regex.cpp:270 ---------
propagate accept: (aut.accept a 1 re.none)
------------------------------------------------
-------- [seq_regex] propagate_accept ../src/smt/seq_regex.cpp:270 ---------
propagate accept: (let ((a!1 (or (= "" b) (= (seq.unit (seq.nth_i a 0)) b))))
  (aut.accept a 1 (ite a!1 re.none (str.to_re ""))))
------------------------------------------------
derivative((seq.nth_i a 1)): (let ((a!1 (or (= "" b) (= (seq.unit (seq.nth_i a 0)) b))))
  (ite a!1 re.none (str.to_re "")))
derivative result: re.none

Abbreviated trace (-tr:seq_regex_brief), simpler but probably only readable to me:

PIR(a,id47) 
PA(a@0,id47) (unfold) n(id47)=(not (= "" b))  (Warning: is_nullable did not simplify)d(id47)=id128 
PA(a@1,id73) (empty) 
PA(a@1,id153) (unfold) d(id153)=id73 

Note the line: Warning: is_nullable did not simplify to true or false
The actual propagation seems simple, only iterates a couple of times. The state graph does not seem to be invoked at all.
The derivative is re.none after only two iterations since the intersection contains a length-1 regex.

[NikolajBjorner]

The example behaves correctly if (assert (= 0 (str.len b))) is replaced by the equivalent (assert (= b "")), suggesting something to do with the interaction between the solver and length constraints.

This is because when b = "" appears at top level, then b gets replaced by "" elsewhere and the regex becomes ground.
This simplification is not yet invoked for (str.len b) = 0. It will thanks to your observation, but I will hold off enabling this simplification until the real bug is fixed.

But the fact these bugs are only present at model validation stage is a bit surprising.

It simply saturates into a state that is not representative of a solution.

Theory seq
Solved equations:
a |-> (str.++ (seq.unit #60) (seq.tail a 0))
b |-> String[]
(str.at a 0) |-> (seq.unit (seq.nth_i a 0))
(seq.tail a 0) |-> String[]
Exclusions:
String[] != (str.at a 0)
b != (seq.unit (seq.nth_i a 0))
(str.len b) [0:0]
(str.len a) [1:1]
(str.len (str.at a 0)) [1:1]
-------------------------------

[zhendongsu]

Refutation soundness issue (in default mode):

[611] % z3release rewriter.pull_cheap_ite=true small.smt2
sat
(
  (define-fun a () String
    "b")
)
[612] % z3release small.smt2
unsat
(error "line 8 column 10: model is not available")
[613] % 
[613] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re
  (ite (str.in_re (ite (str.in_re a (re.* (re.union (str.to_re "a") (str.to_re "b")))) a "")
        (re.* (re.union (re.inter (re.range a "u") (str.to_re "b")) (str.to_re "a")))) a "")
  (str.to_re "b")))
(check-sat)
(get-model)
[614] % 

Commit: c0e74f9

[zhendongsu]

Another invalid model instance (in default mode):

[586] % z3release model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(
  (define-fun a () String
    "")
)
[587] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
  (re.++ (re.* re.allchar)
   (re.++
    (str.to_re
     (ite (ite (str.in_re a (re.+ (str.to_re "A"))) true (= a "AA")) a "A"))
    (re.* re.allchar)))))
(check-sat)
(get-model)
[588] % 

Commit: c0e74f9

[zhendongsu]

Invalid model instance (in default mode):

[563] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun c () String
    "CAB")
  (define-fun a () Bool
    true)
  (define-fun d () String
    "CAB")
  (define-fun b () Int
    5)
)
[564] % 
[564] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Int)
(declare-fun c () String)
(declare-fun d () String)
(assert (= c (str.++ (str.replace d (str.substr (ite a c d) 0 b) c) d)))
(check-sat)
(get-model)
[565] % 

Commit: c0e74f9

[zhendongsu]

Invalid model instance (in default mode):

[578] % z3release model_validate=true small.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
  (define-fun f () Bool
    true)
  (define-fun h () String
    "C")
  (define-fun b () String
    "ACA")
  (define-fun a () String
    "A")
  (define-fun d () String
    "B")
  (define-fun e () Bool
    true)
  (define-fun c () String
    "C")
  (define-fun g () Bool
    false)
)
[579] % 
[579] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun g () Bool)
(declare-fun h () String)
(assert (= b (str.++ (ite (= c h) a h) (ite (= e f) "A" "") (ite g h "") (ite (= d "") c h))))
(assert (= g (= (ite e "A" c) b)))
(check-sat)
(get-model)
[580] % 

Commit: c0e74f9

It reproduces for at least as early as z3 4.8.5 and later.

[rainoftime]

c0e74f9

(set-option :model_validate true)
(declare-fun v16 () Bool)
(declare-fun i5 () Int)
(declare-fun str7 () String)
(push)
(assert v16)
(assert (distinct "ed\u01a5\u01f1\u0241\xa8{r\u01ef\u02" str7 (str.from_int i5)))
(push)
(pop)
(check-sat)

z3 delta.out.smt2
(error "line 8 column 5: exponent is too big")
sat
(error "line 10 column 10: an invalid model was generated")

[rainoftime]

(set-option :model_validate true)
(set-option :smt.arith.eager_eq_axioms false)
(set-option :smt.random_seed 1)
(declare-fun v4 () Bool)
(declare-fun v8 () Bool)
(declare-fun v15 () Bool)
(declare-fun i4 () Int)
(declare-fun i10 () Int)
(declare-fun str7 () String)
(declare-fun str8 () String)
(declare-fun str10 () String)
(declare-fun str14 () String)
(declare-fun str16 () String)
(assert (and v15 (= v4 v8)))
(assert (str.contains str10 str16))
(push)
(assert (distinct str16 (str.++ str8 str14) str10 "fCr" (str.substr str7 9 i4)))
(push)
(assert (< i10 1))
(assert (< i10 2))
(assert (< i10 0))
(check-sat)
(pop)
(check-sat)

z3 delta.out.smt2
sat
sat
(error "line 24 column 10: an invalid model was generated")

[wintered]

Commit: a6ef99d

$z3release model_validate=true delta.out.smt2
sat
(error "line 32 column 10: an invalid model was generated")
$cat delta.out.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun T0_6 () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun T3_6 () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () String)
(declare-fun v () Bool)
(declare-fun o () Bool)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun u () String)
(declare-fun w () Bool)
(assert (= r (not (= d 0))))
(assert (ite r (and w (= d a) (= u i) (= T3_6 g) (= j "") (= a (str.len g)) (= u (str.++ g f)) 
(not (str.in_re i (str.to_re "")))) true))
(assert true)
(assert (= t (not v)))
(assert (ite t (and s q p o (= l "") (= 3 (str.len T0_6)) (= u (str.++ e e)) 
(= g (str.++ k h))) (= 3 (str.len T0_6))))
(assert (not (= "" u)))
(assert (< 0 d))
(assert (< 0 c))
(check-sat)
$

[zhendongsu]

Segfault with release build and assertion failure with debug build (append here since the instance is a string formula):

[528] % z3-4.8.10 small.smt2
sat
[529] % z3release small.smt2
Segmentation fault
[530] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 170
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[531] % 
[531] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun p () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun q () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () Bool)
(declare-fun m () Bool)
(declare-fun n () Bool)
(declare-fun o () String)
(assert
 (ite m
  (and (= c a) (= o e)
   (not (ite n
         (and (= d b) (= q k) (not (str.in_re i (re.++ (str.to_re "m") (re.range "6" "7")))))
         (= f ""))))
  (str.in_re h (str.to_re (ite (= o (str.++ p f)) "2" j)))))
(assert
 (ite n
  (and (= f (ite l (ite (= a 0) g e) "9"))
   (not (str.in_re i (re.++ (str.to_re (ite (= c 1) "." "b")) (str.to_re "="))))) false))
(assert (not (= f "6")))
(check-sat)
[532] % 

Commit: a6ef99d

[zhendongsu]

An invalid model instance (in default mode):

[541] % z3-4.8.10 model_validate=true small.smt2
sat
(
  (define-fun a () String
    "uuuuuuuu\x00")
)
[542] % z3release model_validate=true small.smt2
sat
(error "line 10 column 10: an invalid model was generated")
(
  (define-fun a () String
    "\u\u\u\u\u\u\u\u{abcd}E")
)
[543] % cat small.smt2
(declare-fun a () String)
(assert
 (ite (= a "\u\u\u\u\u\u\u\u")
  (str.in_re a (re.* re.allchar))
  (str.in_re a
   (re.++
    (str.to_re
     (ite (str.in_re a (str.to_re "\u\u\u\u\u\u\u\u")) a "\u\u\u\u\u\u\u\u"))
    (re.* re.allchar)))))
(check-sat)
(get-model)
[544] % 

Commit: a6ef99d

[rainoftime]

a6ef99d

(set-option :model_validate true)
(set-option :smt.arith.eager_eq_axioms false)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(declare-fun str8 () String)
(declare-fun str10 () String)
(declare-fun str11 () String)
(declare-fun str12 () String)
(declare-fun v19 () Bool)
(assert (= v19 (and (= str2 str10) (= str2 str7))))
(assert (distinct str11 str3 "u0" str8))
(assert (= (= v19 (and v19 (= str2 str10))) (and (= str11 (str.++ str8 str6)) (= (str.++ str8 str6) (str.++ str12 str3 str2)))))
(push)
(check-sat)
(pop)
(check-sat)

z3 delta.out.smt2 
sat
sat
(error "line 18 column 10: an invalid model was generated")

[zhendongsu]

Solution soundness issue:

[542] % z3-4.8.10 small.smt2
sat
[543] % z3release small.smt2
sat
[544] % cvc4 -q small.smt2
unsat
[545] % 
[545] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
  (re.diff re.allchar
   (re.++ (re.* re.allchar)
    (str.to_re (ite (str.in_re a re.allchar) a ""))))))
(check-sat)
[546] %

Commit: a6ef99d

[zhendongsu]

Refutation soundness issue:

[562] % cvc4 -q --strings-exp --produce-models small.smt2
sat
(
(define-fun var_9 () String "")
(define-fun var_10 () String "zb")
)
[563] % z3release small.smt2
unsat
(error "line 25 column 10: model is not available")
[564] %
[564] % z3release model.smt2
sat
( 
  (define-fun var_10 () String
    "zb")
  (define-fun var_9 () String
    "")
)
[565] %
[565] % cat small.smt2
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(assert (str.in_re (str.++ var_9 "z" var_10) (re.++ (re.* (re.union
  (str.to_re "z") (re.opt (re.++ (str.to_re "b") (re.* (str.to_re
  "b")))))) (str.to_re "b"))))
(assert (str.in_re (str.++ var_9 "z" var_10) (re.++ (re.* (re.union
  (re.opt (re.union (str.to_re "z") (str.to_re "u"))) (re.++
  (str.to_re "b") (re.++ (re.* (str.to_re "b")) (re.union (str.to_re
  "z") (str.to_re "a")))))) (re.++ (str.to_re "b") (re.* (str.to_re
  (str.replace_all (str.++ var_9 "z" var_10) var_9 var_10)))))))
(assert (str.in_re (str.++ (str.replace_all (ite (str.in_re ""
  (str.to_re "a")) var_9 var_10) (ite (str.in_re "" (str.to_re "a"))
  var_9 var_10) var_10) "z" var_10) (re.++ (re.* (re.union (str.to_re
  "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union
  (str.to_re "z") (str.to_re (str.at var_9 (str.len var_10)))))))
  (re.union (str.to_re "b") (str.to_re "a")))))
(assert (str.in_re (str.substr (ite (str.in_re var_10 (re.* (re.range
  "a" "u"))) "" "b") 0 (str.len (str.from_code 0))) (re.* (re.range
  "a" "u"))))
(assert (str.in_re var_9 (re.* (re.union (str.to_re "a") (re.*
  (re.range "a" "u"))))))
(assert (not (str.< (str.++ var_9 (ite (str.in_re var_9 (str.to_re
  (str.++ var_9 "z"))) var_10 var_9) var_10) "z")))
(check-sat)
(get-model)
[566] %

Commit: a6ef99d

[rainoftime]

887b62e

(set-option :model_validate true)
(set-option :rewriter.eq2ineq true)
(declare-fun v4 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str7 () String)
(assert (and v8 (str.in_re (str.++ str5 str4 str3 str7 str3) (re.+ (str.to_re "rl")))))
(assert (str.contains str0 str5))
(push)
(declare-fun v49 () Bool)
(assert (not (str.in_re str7 (str.to_re str3))))
(assert (and v7 (str.prefixof str1 str3) (= v4 v49)))
(check-sat)

z3 delta.out.smt2 
sat
(error "line 18 column 10: an invalid model was generated")

[rainoftime]

(set-option :model_validate true)
(set-option :smt.arith.eager_eq_axioms false)
(set-option :rewriter.flat false)
(set-option :rewriter.blast_distinct true)
(set-option :smt.phase_selection 2)
(declare-fun v1 () Bool)
(declare-fun i11 () Int)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(push)
(assert (or true (str.prefixof str4 (str.++ (str.++ str7 str7) (str.from_int 1)))))
(assert (> i11 43))
(assert (or (distinct str3 "" str6 (str.++ str5 (str.from_int i11))) (and v1 (= str4 (str.++ str4 str2)) (= str5 (str.++ str7 str4)) (= str2 (str.++ str6 str2)))))
(check-sat)
(push)
(assert (or v1 (str.contains (str.++ str7 str5) str6)))
(check-sat)
(assert (not (= str6 str4)))
(check-sat)

z3 delta.out.smt2 
sat
sat
sat
(error "line 23 column 10: an invalid model was generated")

[NikolajBjorner]

@veanes Did you have a chance to look into these?
Here are some observations:

When solving:

(declare-fun a () String)
(declare-fun b () String)
(set-option :model_validate true)
(assert (str.in_re a
     (re.diff (re.union (re.* (str.to_re "b")) (str.to_re "z")) (re.++ (re.* (str.to_re "z")) (str.to_re b)))))
(assert (= 0 (str.len b)))
(check-sat)
(get-model)

Search reaches a point where it propagates

propagate accept: (let ((a!1 (or (= "" b) (= (seq.unit (seq.nth_i a 0)) b))))
  (aut.accept a 1 (ite a!1 re.none (str.to_re ""))))

In response it creates the single axiom:

assert:(not (aut.accept a 1 (if (or #65 #141) re.none (str.to_re String[]))))
(<= (str.len a) 1)
(aut.accept a 2 re.none)

This axiom is insufficient to enforce that when 'a' has length 1, then the condition of the
disjunction

(or (= "" b) (= (seq.unit (seq.nth_i a 0)) b)))

must be false.
Tracing the code in

void seq_regex::propagate_accept(literal lit) {

we see that for this case, the is_nullable check is skipped.
There are no conditions to esure that the regex

 (ite (or (= "" b) (= (seq.unit (seq.nth_i a 0)) b))) re.none (str.to_re ""))))

accepts the empty string. It needs to be enforced to handle the case where a has length 1.
The reason why the nullable check is skipped is that min_length test:

     if (min_len == 0) {
            expr_ref is_nullable = is_nullable_wrapper(r);

is skipped, min_length is UINT_MAX. Indeed, the code for computing "info" has a case where it handles ite expressions.

    expr* c, * t, * f;
    if (u.m.is_ite(e, c, t, f)) {
        i1 = get_info_rec(t);
        i2 = get_info_rec(f);
        return i1.orelse(i2);
    }

The definition of "orelse" uses the min_length attribute from i1 but ignores the min_length from i2.
Seems it should have computed a "min" over these attributes.

seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) const {
    if (is_known()) {
        if (i.is_known()) {
            // unsigned ite_min_length = std::min(min_length, i.min_length);
            // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef);
            // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
            return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height));
        }
        else
            return i;
    }
    else
        return *this;
}

Thus, it would seem the way info is computed and how it gets used needs a revision.
Could you take a closer look given this context?

[zhendongsu]

Commit: 30e904b

Another solution unsoundness instance:

[547] % z3release small.smt2
sat
[548] % cvc4 -q small.smt2
unsat
[549] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
  (re.diff (re.++ (re.* (str.to_re "b")) (str.to_re "a"))
   (str.to_re a)
   (re.++ (str.to_re "a") (str.to_re a)))))
(check-sat)
[550] % 

[zhendongsu]

Commit: 51a4db8

Another (likely related) instance:

[550] % z3release model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
(
  (define-fun y () String
    "")
  (define-fun x () String
    "A")
)
[551] % 
[551] % cat small.smt2
(declare-fun x () String)
(declare-fun y () String)
(assert (str.in_re x (re.diff (re.union (str.to_re "AB") (str.to_re "C")) (str.to_re "A") (str.to_re y))))
(check-sat)
(get-model)
[552] % 

[rainoftime]

f942c3d

(set-option :smt.arith.eager_eq_axioms false)
(declare-fun y () Int)
(declare-fun c () (Seq Int))
(declare-fun b () (Seq Int))
(assert (and (> y 0) (not (= (seq.nth b 1) (seq.nth c y)))))
(check-sat)

[NikolajBjorner]

bugs are re-triaged based on fix by @veanes. Several bugs are duplicates either of the fix or of a separate fix during model construction. Bugs that are still valid are marked with a "sad" face.

[zhendongsu]

Commit: 3a5b88e
OS: Ubuntu 18.04
Note: (1) The latest commit detects the produced invalid model (while z3-4.8.10 does not); (2) it also outputs l_undef, which might be for debugging use.

[545] % z3-4.8.10 rewriter.cache_all=true model_validate=true small.smt2
sat
[546] % z3release rewriter.cache_all=true model_validate=true small.smt2
l_undef
sat
(error "line 14 column 10: an invalid model was generated")
[547] % 
[547] % cvc5 -q small.smt2
unsat
[548] % 
[548] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert
 (str.in_re (str.++ a "z" b)
  (re.++ (re.union (re.* (str.to_re "z")) re.none)
   (re.++ (re.* (re.* (re.* (str.to_re "z"))))
    (re.union
     (re.inter (re.++ (re.* (str.to_re "z")) (str.to_re "a"))
      (str.to_re (str.replace "" (str.++ a "") (str.++ "" ""))))
     (str.to_re "a"))))))
(assert
 (xor (str.in_re b (re.* (re.union (str.to_re "a") re.none)))
  (str.in_re b (re.range "a" "u"))))
(check-sat)
[549] % 

[zhendongsu]

Commit: 082ec0f
OS: Ubuntu 18.04

Refutation soundness issue (a="" is a model):

[583] % z3-4.8.10 small.smt2
sat
[584] % cvc5 -q --strings-exp small.smt2
sat
[585] % z3release small.smt2
unsat
[586] % 
[586] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (str.to_re "a"))))
(assert (str.in_re a (re.* (str.to_re "b"))))
(assert
 (ite (str.in_re a (re.* (re.comp (str.to_re ""))))
  (= a "")
  (str.in_re (str.++ "aaab" a)
   (re.*
    (re.++ (re.comp (re.* (str.to_re "b")))
     (str.to_re (str.from_int (str.len a))))))))
(check-sat)
[587] % 

[zhendongsu]

Commit: 2138ef2
OS: Ubuntu 18.04

Solution unsoundness:

[738] % z3release small.smt2
sat
unsat
[739] % cat small.smt2
(declare-fun num1 () String)
(declare-fun num2 () String)
(assert (ite (str.prefixof "-" (str.at num2 0)) false (not (= (- 1) (str.to_int (str.at num2 (- (str.len num2) 4)))))))
(assert (not (>= (ite (str.prefixof "-" (str.at num2 0)) 0 (str.to_int (str.at num2 (- (str.len num2) 3)))) 10)))
(assert (ite (str.prefixof "-" (str.at num2 (- (str.len num2) 3))) (> (str.len (str.at num2 0)) 1) (not (= (- 1) (str.to_int (str.at num2 0))))))
(assert (>= (- (str.len num2) 3) 0))
(assert (not (>= (ite (str.prefixof "-" (str.at num2 0)) 0 (str.to_int (str.at num2 (- (str.len num2) 2)))) 10)))
(assert (ite (str.prefixof "-" (str.at num2 (- 2))) true (not (= 0 (str.to_int (str.at num2 (- (str.len num2) 2)))))))
(assert (> 2 (str.len num1)))
(assert (< (ite (< (str.len num1) (str.len num2)) (str.len num1) (str.len num2)) 2))
(assert (>= (+ (ite (str.prefixof "-" (str.at num1 (- (str.len num1) 1))) (- (str.to_int (str.substr (str.at num1 0) 1 0))) (str.to_int (str.at num1 (- (str.len num1) 1))))
             (ite (str.prefixof "-" (str.at num2 0)) 0 (str.to_int (str.at num2 (- (str.len num2)))))) 10))
(assert (ite (str.prefixof "-" (str.at num2 (- (str.len num2) 1))) (> (str.len (str.at num2 (- (str.len num2) 1))) 1) (not (= 0 (str.to_int (str.at num2 (- (str.len num2) 1)))))))
(assert (>= (ite (< (str.len num1) (str.len num2)) (str.len num1) (str.len num2)) 1))
(assert (ite (str.prefixof "-" num2) (and (not (= 0 (str.to_int (str.substr num2 1 (- (str.len num2) 1))))) (> (str.len num2) 1)) (not (= (- 1) (str.to_int num2)))))
(assert (not (= (str.len num2) 0)))
(assert (ite (str.prefixof "-" num1) (> (str.len num1) 1) (not (= (- 1) (str.to_int num1)))))
(assert (not (= (str.len num1) 0)))
(check-sat-using (then nnf qe2 smt))
(check-sat)
[740] % 

[zhendongsu]

Commit: 2138ef2
OS: Ubuntu 18.04
Related: #5140 (comment)

Invalid model:

[580] % z3-4.8.10 model_validate=true small.smt2
sat
(
  (define-fun b () String
    "")
  (define-fun a () String
    "zbz")
)
[581] % z3release model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(
  (define-fun b () String
    "bzz")
  (define-fun a () String
    "")
)
[582] % cat small.smt2
(set-option :rewriter.cache_all true)
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.++ a "z" b) (re.++ (re.* (re.+ (re.union
  (str.to_re "z")))) (re.++ (ite (str.in_re b (re.++ (re.* (re.union
  (re.union (str.to_re "aaa") (re.* (str.to_re ""))))) (re.++
  (str.to_re "b")))) (str.to_re "z") (re.+ (str.to_re "b"))) (re.*
  (str.to_re "a"))))))
(check-sat)
(get-model)
[583] % 

[zhendongsu]

Commit: 2138ef2
OS: Ubuntu 18.04
Note: z3-4.8.10 outputs the same invalid model, but the model validator fails to detect it.

Invalid model:

[566] % z3-4.8.10 model_validate=true small.smt2
sat
(
  (define-fun a () String
    "ABA")
)
[567] % z3release model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(
  (define-fun a () String
    "ABA")
)
[568] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re a
  (re.+
   (re.++ (str.to_re "AA")
    (ite (str.in_re a (re.++ (str.to_re a) (re.union (str.to_re "A") (str.to_re "B"))))
     (re.union (str.to_re "A") (str.to_re ""))
     (re.union (str.to_re "A") (str.to_re "B")))))))
(check-sat)
(get-model)
[569] % 

[zhendongsu]

Commit: 2138ef2
OS: Ubuntu 18.04

(1) Refutation unsoundness with smt.threads=2, and (2) invalid model in the default mode:

[607] % z3release model_validate=true small.smt2
sat
(error "line 17 column 10: an invalid model was generated")
[608] % z3release smt.threads=2 model_validate=true small.smt2
unsat
[609] % cvc5 -q small.smt2
sat
[610] % cat small.smt2
(declare-fun s () String)
(assert
 (str.in_re s
  (re.++
   (re.union
    (re.inter (re.opt (str.to_re "a")) (str.to_re ""))
    (str.to_re "b"))
   (re.diff (str.to_re "b") (str.to_re ""))
   (str.to_re "AA")
   (ite
    (str.in_re s
     (re.++ (str.to_re (str.replace s "" ""))
      (re.diff (re.opt (str.to_re "b")) (str.to_re ""))))
    (re.union (str.to_re "a") (str.to_re ""))
    (re.++ (str.to_re "aa")
     (re.* (re.union (str.to_re (str.++ "b" s)) (str.to_re s))))))))
(check-sat)
[611] % 

[zhendongsu]

Commit: 2138ef2
OS: Ubuntu 18.04

Another invalid model instance:

[546] % z3-4.8.10 model_validate=true small.smt2
sat
(
  (define-fun b () String
    "ab")
  (define-fun a () String
    "a")
)
[547] % z3release model_validate=true small.smt2
sat
(error "line 10 column 10: an invalid model was generated")
(
  (define-fun b () String
    "b")
  (define-fun a () String
    "a")
)
[548] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.++ a "z" b) (re.++ (re.* (re.union (str.to_re "z") (str.to_re "a"))) (str.to_re "b"))))
(assert (str.in_re (str.++ a "z" b) (re.++ (re.* (re.union (str.to_re
   "z") (re.++ (re.union (str.to_re "b") (str.to_re "a")) (re.union
   (str.to_re "z") (str.to_re "b"))))) (ite (str.in_re b (re.*
   (str.to_re "z"))) (re.* (re.union (str.to_re "z"))) (re.union
   (str.to_re "z") (re.++ (re.union (str.to_re "b") (str.to_re "a"))
   (re.union (str.to_re "z") (str.to_re "b"))))))))
(check-sat)
(get-model)
[549] % 

[zhendongsu]

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] %

moved to #5467

[rainoftime]

Invalid model at 45228bf

(declare-const x2 Bool)
(declare-const x1 Bool)
(declare-const x3 Bool)
(declare-fun y () Int)
(declare-fun c () (Seq Int))
(declare-fun x () Int)
(declare-fun b () (Seq Int))
(declare-fun l () Bool)
(declare-fun l1 () Bool)
(declare-fun l18 () Bool)
(assert (and (or x3 x2) (= (seq.nth b 0) (seq.nth c x)) (distinct (seq.nth b y) (seq.nth c y))))
(assert (= l x1))
(check-sat-assuming (l1 l18))
(check-sat)

z3 model_validate=true xx.smt2
sat
sat
(error "line 14 column 10: an invalid model was generated")

[zhendongsu]

Commit: d5c6abe
OS: Ubuntu 18.04

Solution soundness issue:

[511] % z3release small.smt2
sat
[512] % cvc5 -q small.smt2
unsat
[513] % cat small.smt2
(declare-fun a () Int)
(assert (= (str.replace_all "-1" "" "") (str.from_int a)))
(check-sat)
[514] % 

[zhendongsu]

One more invalid model instance:

[630] % z3release model_validate=true small.smt2
sat
sat
(error "line 4 column 10: an invalid model was generated")
(
  (define-fun a () String
    "BABBACAA")
)
[631] % cat small.smt2
(declare-const a String)
(check-sat)
(assert (str.in_re a (re.++ (str.to_re "BBBA") re.allchar (ite (str.in_re a (re.++ (re.* re.allchar) (str.to_re "A") (str.to_re "B"))) (str.to_re "B") (str.to_re "A")) (str.to_re "AA"))))
(check-sat)
(get-model)
[632] % 

[zhendongsu]

Refutation soundness issue:

[560] % cvc5 -q small.smt2
sat
[561] % z3release small.smt2
unsat
[562] % z3-4.8.10 small.smt2
unsat
[563] % cat small.smt2
(declare-fun s () String)
(assert
 (not
  (str.in_re (str.++ s "BA")
   (re.*
    (re.union (str.to_re "AB")
     (re.++ (re.union (str.to_re "A") (str.to_re "B"))
      (re.union (str.to_re "B") (str.to_re (str.replace_all "B" "A" "")))))))))
(check-sat (= s ""))
[564] % 

[zhendongsu]

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] % 

moved to #5467

[NikolajBjorner]

NB: this one is still open

(declare-fun a () String)
(assert
 (str.in_re
  (ite (str.in_re (ite (str.in_re a (re.* (re.union (str.to_re "a") (str.to_re "b")))) a "")
        (re.* (re.union (re.inter (re.range a "u") (str.to_re "b")) (str.to_re "a")))) a "")
  (str.to_re "b")))
(check-sat)
(get-model)

Other reports also not checked with eyes should be examined.

[veanes]

I investigated this one more closely. If I rewrite it in a more human-readable form it says (using X for a):
(if (if X in ("a"|"b")* then X else "") in (([X - "u"] & "b")|"a")* then X else "") in "b"

it currently gives the model X="b" in the latest changes (that is correct -- unless I made a typo somewhere). Observe that ["b"-"u"]&"b" = "b"
(tried also different random seeds, as well as unsat variations of it e.g. with range [X - "a"] instead of [X - "u"])
so seems to be correct to me.
(from the comment on Apr 3, the incorrect answer used to be unsat)

[veanes]

As I was investigating an incorrect unsat above (the case (1) below) I found a weird behavior (1) is unsat (incorrect), but (2) is sat, the only difference between (1) and (2) is that in (1) the uninterpreted symbol is named lower case 'a', in (2) it is named uppercase 'X', as to why that would make any difference -- I don't know, but answers did not change with different random seeds. It seemed pretty consistent that uppercase naming produced the answer sat while lowercase naming produced the answer unsat.

(declare-fun a () String)
(assert (str.in_re a (re.* (str.to_re "a"))))
(assert (str.in_re a (re.* (str.to_re "b"))))
(assert
(ite (str.in_re a (re.* (re.comp (str.to_re ""))))
(= a "")
(str.in_re (str.++ "aaab" a)
(re.*
(re.++ (re.comp (re.* (str.to_re "b")))
(str.to_re (str.from_int (str.len a))))))))
(check-sat)

(above is from June 10)

(declare-fun X () String)
(assert (str.in_re X (re.* (str.to_re "a"))))
(assert (str.in_re X (re.* (str.to_re "b"))))
(assert
(ite (str.in_re X (re.* (re.comp (str.to_re ""))))
(= X "")
(str.in_re (str.++ "aaab" X)
(re.*
(re.++ (re.comp (re.* (str.to_re "b")))
(str.to_re (str.from_int (str.len X))))))))
(check-sat)

[NikolajBjorner]

typically it is possible to force divergent behavior using different random seeds, but for the above example, the "X" example and "a" example behave differently across different seeds. They induce different hash values so the order of identifiers will be different and then pre-processing and solving can diverge. Even the result of pre-processing is different (seen by adding -tr:asserted_formulas in debug mode) so this is where I would start an investigation.

[veanes]

thx for the clarification. I'll continue to investigate this one.

[zhendongsu]

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] %

moved to #5467

[zhendongsu]

Commit: 5652d2a
OS: Ubuntu 18.04

Segfault (appears to be a recent regression):

[511] % z3-4.8.11 small.smt2
sat
[512] % z3release small.smt2
Segmentation fault
[513] % z3debug small.smt2
Segmentation fault
[514] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==30248==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55ef958bd40b bp 0x7ffd577587b0 sp 0x7ffd577587b0 T0)
==30248==The signal is caused by a READ memory access.
==30248==Hint: address points to the zero page.
    #0 0x55ef958bd40a in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x55ef958bd40a in expr::get_sort() const ../src/ast/ast.cpp:406
    #2 0x55ef958c129b in basic_decl_plugin::join(unsigned int, expr* const*) ../src/ast/ast.cpp:1036
    #3 0x55ef959022d9 in basic_decl_plugin::mk_func_decl(int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1119
    #4 0x55ef958fb121 in ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1935
    #5 0x55ef958fb121 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1941
    #6 0x55ef958fb121 in ast_manager::mk_app(int, int, expr*, expr*) ../src/ast/ast.cpp:1957
    #7 0x55ef9488902c in ast_manager::mk_eq(expr*, expr*) ../src/ast/ast.h:2124
    #8 0x55ef9488902c in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3350
    #9 0x55ef94885f66 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2866
    #10 0x55ef94886c3e in seq_rewriter::mk_derivative_rec(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3263
    #11 0x55ef94885f66 in seq_rewriter::mk_derivative(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:2866
    #12 0x55ef9488c24c in seq_rewriter::mk_re_derivative(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:2755
    #13 0x55ef94895882 in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:542
    #14 0x55ef949f3ca7 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:249
    #15 0x55ef949f3ca7 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:646
    #16 0x55ef94a077d6 in process_app<false> ../src/ast/rewriter/rewriter_def.h:303
    #17 0x55ef94a077d6 in resume_core<false> ../src/ast/rewriter/rewriter_def.h:774
    #18 0x55ef94a077d6 in main_loop<false> ../src/ast/rewriter/rewriter_def.h:733
    #19 0x55ef94a077d6 in operator() ../src/ast/rewriter/rewriter_def.h:813
    #20 0x55ef94a0abae in operator() ../src/ast/rewriter/rewriter.h:356
    #21 0x55ef94a0abae in th_rewriter::operator()(obj_ref<expr, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:901
    #22 0x55ef934cd3ab in smt::seq_regex::rewrite(obj_ref<expr, ast_manager>&) ../src/smt/seq_regex.cpp:37
    #23 0x55ef934cd3ab in smt::seq_regex::derivative_wrapper(expr*, expr*) ../src/smt/seq_regex.cpp:465
    #24 0x55ef934dfb58 in smt::seq_regex::propagate_accept(sat::literal) ../src/smt/seq_regex.cpp:340
    #25 0x55ef930ba249 in smt::theory_seq::assign_eh(unsigned int, bool) ../src/smt/theory_seq.cpp:3000
    #26 0x55ef92a4ef0a in smt::context::propagate_atoms() ../src/smt/smt_context.cpp:1342
    #27 0x55ef92a5e3dc in smt::context::propagate() ../src/smt/smt_context.cpp:1701
    #28 0x55ef92a627df in smt::context::init_assumptions(ref_vector<expr, ast_manager> const&) ../src/smt/smt_context.cpp:3267
    #29 0x55ef92a68089 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3559
    #30 0x55ef92a68d11 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3497
    #31 0x55ef9267b26f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic_core.cpp:201
    #32 0x55ef94507355 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:119
    #33 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #34 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #35 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #36 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #37 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #38 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #39 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #40 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #41 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #42 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #43 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #44 0x55ef944fc9e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1038
    #45 0x55ef94507355 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:119
    #46 0x55ef944c5e5e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #47 0x55ef944c7807 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #48 0x55ef94317b18 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #49 0x55ef9433abdf in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #50 0x55ef94353604 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #51 0x55ef943289d6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #52 0x55ef942a35c5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1647
    #53 0x55ef94200a83 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #54 0x55ef94200a83 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #55 0x55ef94200a83 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3141
    #56 0x55ef941b5c65 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3190
    #57 0x55ef914fbfdf in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #58 0x55ef914a6894 in main ../src/shell/main.cpp:371
    #59 0x7f7296d50b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #60 0x55ef914bc789 in _start (/local/suz-local/software/z3san/build-07252021115942-5652d2a/z3+0x209789)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
==30248==ABORTING
[515] % 
[515] % cat small.smt2
(declare-const a String)
(assert (str.in_re a (re.* (str.to_re (str.from_int (str.len a))))))
(check-sat)
[516] % 

[zhendongsu]

Solution unsoundness (a recent regression from z3-4.8.12):

[587] % z3-4.8.12 model_validate=true small.smt2
unsat
(error "line 5 column 10: model is not available")
unsat
[588] % z3release model_validate=true small.smt2
sat
(
  (define-fun a () String
    "")
)
unsat
[589] % cat small.smt2
(declare-const a String)
(assert (str.in_re (str.replace_all (str.++ a (ite (= a "") a "") "ab") (str.++ a (ite (= a "") a "") "ab") "1") (re.* (str.to_re (str.from_int (- (+ (str.len a) 1)))))))
(assert (= a ""))
(check-sat)
(get-model)

(reset)

(define-fun a () String "")
(assert (str.in_re (str.replace_all (str.++ a (ite (= a "") a "") "ab") (str.++ a (ite (= a "") a "") "ab") "1") (re.* (str.to_re (str.from_int (- (+ (str.len a) 1)))))))
(assert (= a ""))
(check-sat)
[590] % 

[zhendongsu]

Invalid model (regression from z3-4.8.10):

[609] % z3release model_validate=true small.smt2
sat
sat
(error "line 16 column 10: an invalid model was generated")
(
  (define-fun b () String
    "")
  (define-fun a () String
    "0bzbzd")
)
[610] % z3-4.8.10 model_validate=true small.smt2
sat
sat
(
  (define-fun b () String
    "!0!")
  (define-fun a () String
    "0bzpbz")
)
[611] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(check-sat)
(assert
 (str.in_re a
  (re.++
   (re.+
    (re.++ (str.to_re "0")
     (re.++ (re.union (str.to_re "b") (str.to_re "a"))
      (re.union (str.to_re "z") (str.to_re "b"))
      (re.range "a" "u"))))
   (ite (<= 0 (str.len b))
    (re.++ (re.union (str.to_re "b") (str.to_re "a"))
     (re.union (str.to_re "z") (str.to_re "b")))
    (str.to_re "b")))))
(check-sat)
(get-model)
[612] %