Consolidated invalid model bugs

[lmaltsis]

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 6 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(declare-const x Real)
(assert (= x 0.0))
(assert (not (= (^ (* x 2.0) (/ 1.0 x))
                (^ (* 0.0 (/ 1.0 x))
                   (* x (/ 1.0 2.0))))))
(check-sat)

Commit: daf2506b

[lmaltsis]

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 5 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(declare-fun +zero () (_ FloatingPoint 3 2))
(declare-fun r () (_ FloatingPoint 3 2))
(assert (fp.eq +zero (fp #b0 #b000 #b1)))
(assert (fp.eq r (fp.fma RTN r +zero (_ +zero 3 2))))
(check-sat)

Commit: daf2506b

[fabiomadge]

Related, but actually produces the wrong result:

; fma(RNE, 1.0, 1.0, +0) should equal 1.0, so this should be unsat.                                                                     
; Z3 folds the fma to 2.0 and returns sat.                                                                               
(assert
  (not (=
    (fp.fma RNE
      (fp #b0 #b011 #b0)   ; x = 1.0  in FP(3,2)
      (fp #b0 #b011 #b0)   ; y = 1.0
      (fp #b0 #b000 #b0))  ; z = +0
    (fp #b0 #b011 #b0))))  ; != 1.0 ?
(check-sat)

[lmaltsis]

$ cat /tmp/bug.smt2
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(assert (distinct false (= ((_ to_fp 11 53) RTZ #xFFFF) (fp #b1 #b10000000000 #x0000000000000))))
(check-sat)

$ z3 model_validate=true /tmp/bug.smt2
Failed to validate b3 12: (= (to_fp[11:53] roundTowardZero bv[65535:16]) (fp bv[1:1] bv[1024:11] bv[0:52])) false
(sat
    -1 none @0
    2 none @0
    -4 none @0
    8 none @0
    9 none @0
[... >60000 characters skipped]
v145  683  -> 683  (= 0) 76:(bit2bool[0] #680) 77:(bit2bool[1] #680) 78:(bit2bool[2] #680) 79:(bit2bool[3] #680) 80:(bit2bool[4] #680) 81:(bit2bool[5] #680) 82:(bit2bool[6] #680) 83:(bit2bool[7] #680) 84:(bit2bool[8] #680) 85:(bit2bool[9] #680) 86:(bit2bool[10] #680) 87:(bit2bool[11] #680) 88:(bit2bool[12] #680) 89:(bit2bool[13] #680) 90:(bit2bool[14] #680) 91:(bit2bool[15] #680) 92:(bit2bool[16] #680) 93:(bit2bool[17] #680) 94:(bit2bool[18] #680) 95:(bit2bool[19] #680) 96:(bit2bool[20] #680) 97:(bit2bool[21] #680) 98:(bit2bool[22] #680) 99:(bit2bool[23] #680) 100:(bit2bool[24] #680) 101:(bit2bool[25] #680) 102:(bit2bool[26] #680) 103:(bit2bool[27] #680) 104:(bit2bool[28] #680) 105:(bit2bool[29] #680) 106:(bit2bool[30] #680) 107:(bit2bool[31] #680) 108:(bit2bool[32] #680) 109:(bit2bool[33] #680) 110:(bit2bool[34] #680) 111:(bit2bool[35] #680) 112:(bit2bool[36] #680) 113:(bit2bool[37] #680) 114:(bit2bool[38] #680) 115:(bit2bool[39] #680) 116:(bit2bool[40] #680) 117:(bit2bool[41] #680) 118:(bit2bool[42] #680) 119:(bit2bool[43] #680) 120:(bit2bool[44] #680) 121:(bit2bool[45] #680) 122:(bit2bool[46] #680) 123:(bit2bool[47] #680) 124:(bit2bool[48] #680) 125:(bit2bool[49] #680) 126:(bit2bool[50] #680) 127:(bit2bool[51] #680)
v146  747  -> 680  (= 13830554455654793216) -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false -2:false 2:true 2:true 2:true 2:true 2:true 2:true 2:true 2:true 2:true 2:true -2:false 2:true
v147  1    -> 1    true
)
b3 12: (= (to_fp[11:53] roundTowardZero bv[65535:16]) (fp bv[1:1] bv[1024:11] bv[0:52])) :=
value obtained from model:  false
value of the root expression:  true
11: (fp bv[1:1] bv[1024:11] bv[0:52]) :=
value obtained from model:  (fp #b1 #b10000000000 #x0000000000000)
value of the root expression:  (fp #b1 #b01111111111 #x0000000000000)

Commit: 51cbbe0

[lmaltsis]

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 9 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(assert (or
(not (= (seq.replace (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2)) (seq.++ (seq.unit 1) (seq.unit 2)) (as seq.empty (Seq Int))) (seq.unit 0)))
(not (= (seq.contains (seq.++ (seq.unit 0) (seq.unit 2) (seq.unit 2)) (seq.++ (seq.unit 1) (seq.unit 3))) false))
(not (= (seq.nth (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 2) (seq.unit 5)) 3) 5))
(not (= (seq.contains (seq.++ (seq.unit (set.singleton 1)) (seq.unit (set.union (set.singleton 2) (set.singleton 1))) (seq.unit (set.singleton 0)))
                      (seq.unit (set.union (set.singleton 1) (set.singleton 1)))) false))

))
(check-sat)

Commit: eefb644

This has some similarities to #9293 which was patched

[lmaltsis]

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 11 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(declare-fun b ((Array Int (Array Int Real)) Int) Bool)
(declare-fun c () (Array Int (Array Int Real)))
(declare-fun d () (Array Int (Array Int Real)))
(declare-fun a3 () (Array Int (Array Int Real)))
(declare-fun a5 () (Array Int (Array Int Real)))
(declare-fun g () (Array Int (Array Int Real)))
(assert (forall ((?a (Array Int (Array Int Real))) (?h Int))
(= (b ?a ?h) (forall ((?i Int)) (= 0 (= (select (a5 ?h) ?i) (select (a3 ?h) 4)))))))
(assert (=  (store c 3 (store (c 4) 2 3))a3 (store d 2 (store (g 3) 5 4))a3))
(assert (not (b c 2)))
(check-sat)

Commit: eefb644

[lmaltsis]

$ z3 model_validate=true /tmp/bug.smt2
sat
(error "line 9 column 10: an invalid model was generated")

$ cat /tmp/bug.smt2
(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun g ((Array Int Int)) Int)
(declare-fun f (Int) Int)
(assert (and (= (store a x x) a) (= (store f y w) b) (not (= (f x) (f y))) (not (= (g a) (g b)))))
(check-sat)
(exit)

f487af3

Note that this bug stems from the fact that f is incorrectly accepted as the first argument for store when it is not an array.

[lmaltsis]

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

$ cat bug.smt2
(declare-fun v () (Seq Int))
(declare-fun va () String)
(declare-fun r () String)
(declare-fun a () String)
(check-sat)
(assert (str.in_re (str.++ a "B") (re.* (str.to_re (str.substr r (str.to_code "a") (str.len a))))))
(check-sat)

Note the str.to_code
652402f