[Consolidated] issues with tactic.default_tactic=smt sat.euf=true

[rainoftime]

Z3 32beb91
Solution soundness

(declare-const v (_ BitVec 1))
(declare-const u (_ BitVec 1))
(declare-const i (_ BitVec 1))
(declare-const j (_ BitVec 1))
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (and (not (= i j)) (not (= u v)) (= (store (store a ((_ zero_extend 31) i) ((_ zero_extend 7) u)) ((_ zero_extend 31) j) (_ bv0 8)) (store a ((_ zero_extend 31) i) ((_ zero_extend 7) v)))))
(check-sat)

[rainoftime]

SEGV ../src/smt/mam.cpp:2316

(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth))))
(declare-sort process$type)
(declare-fun null () resource$type)
(declare-fun S$mem (process$type S$t$type) BOOL)
(assert (exists ((create$r resource$type)) (exists ((handles (Array resource$type S$t$type))) (exists ((ref (Array process$type resource$type))) (or (= create$r null) (exists ((p process$type) (r resource$type)) (or (= r (ref p)) (= Truth (S$mem p (handles r))))))))))
(check-sat-using ctx-solver-simplify)

NOTE: this one does not need the options tactic.default_tactic=smt sat.euf=true

[rainoftime]

Refutation soundness

(assert (let (($x17 (not (fp.eq (fp (_ bv0 1) (_ bv1 11) (_ bv0 52)) (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)))))) $x17))
(check-sat)

---

(declare-fun t () (_ BitVec 5))
(declare-fun s () (_ BitVec 5))
(declare-fun l1 () Bool)
(assert (let ((?x16 t)) (let ((?x22 t)) (let ((?x6 ((_ extract 4 4) s))) (let (($x20 l1)) (let (($x25 l1)) (let ((?x32 (ite (or false true) (ite (= (bvurem (ite (= ?x6 (_ bv1 1)) (bvneg s) s) (ite (= ((_ extract 4 4) t) (_ bv1 1)) (bvneg t) t)) (_ bv0 5)) (_ bv0 5) (bvadd (bvneg (bvurem (ite (= ?x6 (_ bv1 1)) (bvneg s) s) t)) t)) (ite true (ite (= t (_ bv0 5)) (_ bv0 5) (bvadd (bvurem (ite (= ?x6 (_ bv1 1)) (bvneg s) s) t) (_ bv0 5))) (_ bv0 5))))) (let (($x24 l1)) (let ((?x23 t)) (not (= (bvsmod s t) (ite (and (= ?x6 (_ bv0 1)) true) (bvurem (ite (= ?x6 (_ bv1 1)) (bvneg s) s) (ite (= ((_ extract 4 4) t) (_ bv1 1)) (bvneg t) t)) ?x32))))))))))))
(assert (let ((?x111 (bvurem_i (ite l1 t t) t))) (let ((?x113 t)) (let ((?x51 t)) (let ((?x119 (bvsmod_i t t))) (let (($x47 l1)) (= l1 (= (bvsmod_i s t) (ite false (bvurem_i (ite (= ((_ extract 4 4) s) (_ bv1 1)) (bvmul (_ bv31 5) s) s) (ite (= ((_ extract 4 4) t) (_ bv1 1)) (bvmul (_ bv31 5) t) t)) (ite false (ite (= (bvurem_i (ite (= ((_ extract 4 4) s) (_ bv1 1)) (bvmul (_ bv31 5) s) s) (ite (= ((_ extract 4 4) t) (_ bv1 1)) (bvmul (_ bv31 5) t) t)) (_ bv0 5)) (_ bv0 5) (bvadd (bvmul (_ bv31 5) (bvurem_i (ite (= ((_ extract 4 4) s) (_ bv1 1)) (bvmul (_ bv31 5) s) s) (ite (= ((_ extract 4 4) t) (_ bv1 1)) (bvmul (_ bv31 5) t) t))) t)) (_ bv0 5)))))))))))
(check-sat)

[rainoftime]

memory leak

(declare-const _v (_ BitVec 1))
(declare-fun f () (Array (_ BitVec 4) (_ BitVec 4)))
(assert (forall ((v (_ BitVec 4))) (forall ((u (Array (_ BitVec 4) (_ BitVec 4)))) (and (distinct (store u v ((_ zero_extend 3) _v)) (store f (_ bv0 4) (_ bv0 4)))))))
(check-sat)

Failed to validate 7 99: (= (store u!4 v!3 bv[1:4]) (const bv[0:4])) false
94: (store u!4 v!3 bv[1:4])
(store ((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) #x1 #x1)
96: (const bv[0:4])
((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0)
unknown

[rainoftime]

src/sat/smt/euf_solver.cpp:215

(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort process$type)
(declare-fun S$mem (process$type S$t$type) BOOL)
(declare-fun ref () (Array process$type resource$type))
(declare-fun handles () (Array resource$type S$t$type))
(declare-fun S$cardinality (S$t$type) Int)
(declare-fun S$empty () S$t$type)
(declare-fun l3 () Bool)
(declare-fun l9 () Bool)
(declare-fun true () Bool)
(assert (or (forall ((y process$type)) true) (forall ((x process$type)) (let (($x17 true)))) false (forall ((s S$t$type)) true) (forall ((x process$type) (s S$t$type)) (= (S$cardinality s) (ite (= (S$mem x s) Truth) (S$cardinality s) (S$cardinality s)))) (exists ((p process$type)) (not (= Truth (S$mem p (select handles (select ref p))))))))
(assert (= l9 (forall ((e process$type)) (not (= Truth (S$mem e S$empty))))))
(assert (= l3 (forall ((p process$type)) (= (S$mem p (select handles (select ref p))) Truth))))
(assert (not true))
(check-sat)

z3  tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_solver.cpp
Line: 215
s().value(lit) == l_true
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Invalid model

(declare-fun val () (_ BitVec 1))
(declare-fun B () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun A () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun sel () Bool)
(assert (and sel (not (= A B)) (or (bvugt (_ bv1 1) val) (= A (store B (_ bv1 1) (_ bv0 1))))))
(check-sat)

[rainoftime]

src/util/obj_hashtable.h:174

(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqe) (invack) (gnte))))
(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type)))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort node$type)
(declare-fun chan3$1 () (Array node$type msg$type))
(declare-fun shrset$1 () (Array node$type BOOL))
(declare-fun chan3 () (Array node$type msg$type))
(assert (not (distinct true (forall ((n node$type)) (let (($x19 (= empty (m_cmd (select chan3 n))))))) (and false (and (not (= Truth (ite true (ite (exists ((n node$type)) (= (m_cmd (select chan3$1 n)) empty)) Truth Falsity) (ite (forall ((n node$type)) (and (not (= Truth (select shrset$1 n))) (not (= (m_cmd (select chan3$1 n)) empty)))) Truth Falsity)))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 174
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[zhendongsu]

Solution unsoundness:

[574] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
[575] % z3release small.smt2 
unsat
[576] % cat small.smt2 
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun g () Real)
(assert (or (not (=> (and (= g 1) (= g 0) (<= 1 c)) (<= a 0))) (and true (and (exists ((f Real)) (forall ((d Real)) (= d 0)))))))
(assert (= b 0))
(check-sat)
[577] % 

[zhendongsu]

Refutation unsoundness:

[504] % cvc5 -q small.smt2
sat
[505] % z3release small.smt2
unknown
[506] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[507] % cat small.smt2
(assert (forall ((x Int)) (distinct (mod 0 x) x)))
(check-sat)
[508] %

[zhendongsu]

Release build segfault; debug build assertion violation:

[557] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Segmentation fault
[558] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
ASSERTION VIOLATION
File: ../src/sat/smt/euf_solver.cpp
Line: 265
n->is_equality()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[559] % cat small.smt2 
(declare-fun a () Bool)
(assert (= 1 (+ 0 (ite (not (not (= (+ 0 (ite a 1 0)) 0))) 0 1))))
(check-sat)
[560] % 

[zhendongsu]

Solution unsoundness:

[523] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
sat
[524] % z3release small.smt2
unsat
[525] % cat small.smt2
(declare-fun a () (_ BitVec 64))
(assert (= (not (fp.geq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv0 64)))) (fp.geq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv0 64)))))
(check-sat)
[526] % 

[zhendongsu]

Refutation unsoundness (possibly related to #5429 (comment)):

[614] % z3release small.smt2 
sat
[615] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
unsat
[616] % cat small.smt2 
(declare-fun a () (_ BitVec 64))
(assert (not (fp.geq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv0 64)))))
(check-sat)
[617] % 

Likely related:

[683] % z3release small.smt2 
sat
[684] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
unsat
[685] % cat small.smt2 
(declare-fun a () Float64)
(assert (= (not (fp.leq a a)) (not (fp.leq a a))))
(check-sat)
[686] % 

[zhendongsu]

Solution unsoundness:

[532] % z3release small.smt2 
unsat
[533] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
[534] % cat small.smt2 
(assert (forall ((a Real)) (exists ((b Real)) (> b (* b a)))))
(check-sat)
[535] % 

[zhendongsu]

failed to verify:

[720] % z3release small.smt2
sat
[721] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (not (exists ((a Real))
       (let ((a!1 (exists ((b Int))
                    (and (>= (to_real b!2) 38.0) (= (to_real b) a)))))
         (not a!1))))
evaluated to false
(params keep_cardinality_constraints true pb.solver solver)
(exists ((a Real))
  (let ((a!1 (exists ((b Int)) (and (>= (to_real b!2) 38.0) (= (to_real b) a)))))
    (not a!1))) |-> 2
true |-> 3
[722] % cat small.smt2
(assert (forall ((a Real)) (exists ((b Int)) (=> (< b 0) (exists ((b Int)) (< b a)) (and (>= b a) (forall ((a Real)) (exists ((b Int)) (= b a))))))))
(check-sat)
[723] % 

[zhendongsu]

Refutation unsoundness:

[551] % z3release small.smt2
sat
[552] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[553] % cat small.smt2
(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(assert
 (forall ((x (_ BitVec 8)))
  (ite
   (distinct (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))
    (xor (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))
     (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))))
   (distinct (not (= (bvlshr x a) b))
    (xor (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))
     (forall ((x (_ BitVec 8)))
      (not (= (bvlshr x a) b))))) (= (bvlshr x a) b))))
(check-sat)
[554] %