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

[rainoftime]

Hi, for the following formula
z3 fb6cd8e

src/sat/smt/q_solver.h:77

(declare-sort u1)
(declare-sort u2)
(declare-fun Concat (Bool u1) u2)
(declare-fun w5 () u2)
(assert (forall ((mod Bool)) (exists ((n2 u2)) (exists ((n1 u1)) (not (= w5 (Concat mod n1)))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_solver.h
Line: 77
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/rewriter/poly_rewriter.h:131

(set-option :smt.arith.reflect false)
(declare-fun x () Real)
(assert (exists ((y Real)) (not (= x y))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/poly_rewriter.h
Line: 131
num_args > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/sat_dual_solver.cpp:130

(declare-fun xI2 () Real)
(assert (forall ((ts244uscore0 Real)) (not (or (= xI2 1.0) (= ts244uscore0 0.0)))))
(check-sat-using aufnira)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 130
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/sat_literal.h:48

(declare-sort worlds)
(declare-fun access (worlds worlds) Bool)
(assert (let (($x12 (forall ((w worlds)) (exists ((v worlds)) (access w v)))))))
(assert (let (($x93 (exists ((w worlds)) (forall ((v worlds)) (not (access w v))))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true
ASSERTION VIOLATION
File: ../src/util/sat_literal.h
Line: 48
var() == v
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/euf_internalize.cpp:280

(set-option :smt.ematching false)
(assert (exists ((a (Array (_ BitVec 1) (_ BitVec 1)))) (forall ((b (Array (_ BitVec 1) (_ BitVec 1)))) (and (not (= a b)) (= (a (_ bv0 1)) (b (_ bv0 1)))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 280
Failed to verify: v != sat::null_bool_var

[rainoftime]

/src/sat/smt/euf_model.cpp:217

(declare-datatypes ((CP 0)) (((cp (b Bool)))))
(define-fun-rec CPToString ((cp CP)) String)
(declare-fun CPFromString (String) CP)
(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
(error "line 2 column 43: invalid expression, unexpected ')'")
ASSERTION VIOLATION
File: ../src/sat/smt/euf_model.cpp
Line: 217
Failed to verify: arg

[rainoftime]

src/ast/rewriter/rewriter_def.h:50

(declare-fun y () (_ BitVec 1))
(assert (forall ((b1 Bool)) (forall ((x (_ BitVec 1))) (and b1 (= x y)))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 50
v->get_sort() == r->get_sort()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/q_eval.cpp:243

(declare-fun p (Bool) Bool)
(assert (forall ((b Bool)) (and (p false) (not (p b)))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_eval.cpp
Line: 243
l_false == compare(n, binding, s, t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/qe/mbp/mbp_plugin.cpp:105

(assert (let (($x11 (forall ((?U Int) (?V Int)) (exists ((?W Int)) (not (= ?V (- ?W ?U)))))))))
(check-sat-using bv)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_plugin.cpp
Line: 105
!m.is_false(eval(fml))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/mpq.h:598

(assert (forall ((?X Real)) (= ?X (/ 1 3))))
(check-sat-using qffd)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/util/mpq.h
Line: 598
is_int(a) && is_int(b)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/rewriter/poly_rewriter.h:142

(set-option :smt.arith.reflect false)
(set-option :rewriter.flat false)
(assert (let (($x16 (exists ((?X Real) (?Y Real) (?Z Real)) (and (= ?Y (- ?Z)) (not (= ?X (- ?Z ?Y)))))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true
ASSERTION VIOLATION
File: ../src/ast/rewriter/poly_rewriter.h
Line: 142
num_args > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/q_eval.cpp:212

(declare-fun f (Int) Int)
(assert (forall ((x Int)) (not (= 1 (f x)))))
(assert (= 1 (f 0)))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true
ASSERTION VIOLATION
File: ../src/sat/smt/q_eval.cpp
Line: 212
l_true == compare(n, binding, s, t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/dlist.h:46

(declare-sort I)
(declare-fun op (I I) I)
(declare-fun e0 () I)
(declare-fun e1 () I)
(assert (exists ((e2 I)) (exists ((e3 I)) (forall ((e4 I)) (let (($x80 true)) (let () (let ((?x79 (op e3 e3))) (let (($x78 (= ?x79 e2))) (let () (let ((?x83 (op e2 e1))) (let (($x85 (and (= e0 (op e4 e4)) true true $x78 (= e1 e0)))) (let (($x95 (= e3 (op e3 e4)))) (let () (let (($x138 (= e3 (op e0 e3)))) (let () (let (($x82 (or (and false $x138)))) (let (($x174 (and false false))) (let (($x118 (or true (or (or $x82 (= ?x79 e3)) $x95) (or (= (op e4 e1) e4) (= (op e3 e4) e4))))) (let (($x71 (= (op e2 e3) e3))) (let ((?x84 (op e3 e2))) (let (($x119 (= ?x84 e3))) (let (($x115 (and $x119 $x71))) (let (($x109 (or (and (= (op e3 e0) e3) $x138) (and (= (op e3 e1) e3) (and (distinct (op e1 e3) e3) true))))) (and (or (or $x109 $x115) (= ?x79 e3) $x95) (or (or (and (= ?x83 e2) (= (op e1 e2) e2)) (or (or $x82 (= ?x79 e3)) $x95)) (or (= (op e4 e1) e4) (= (op e3 e4) e4))) $x85))))))))))))))))))))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/util/dlist.h
Line: 46
elem == list
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/euf_invariant.cpp:59

(set-option :sat.branching.heuristic chb)
(declare-sort $$unsorted)
(declare-sort mu)
(declare-fun meq_ind (mu mu $$unsorted) Bool)
(assert (not (= meq_ind (lambda ((X mu) (Y mu) (W $$unsorted)) (= X Y)))))
(declare-fun mtrue ($$unsorted) Bool)
(assert (= mtrue (lambda ((W $$unsorted)) true)))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_invariant.cpp
Line: 59
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/q_mam.cpp:3783

(declare-fun h () Real)
(declare-fun o () Real)
(assert (let (($x56 (not (= o (/ 1.0 h)))))))
(assert (let (($x82 (exists ((j Real)) (let () (or (< 0.0 1.0) (> h 0.0) (= 0.0 (* o j)))))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 3783
t->has_candidates()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/arith_solver.cpp:594

(assert (forall ((value2 String)) (forall ((key2 String)) (let (($x138 (and (not (= (ite (= key2 "a") 1 0) 0)) (or (and (and (= (ite (= 0 (str.len value2)) 1 0) 0) true) true) (not (= (ite (str.prefixof value2 "") 1 0) 0)))))) (and (and (not (= (ite (= key2 "a") 1 0) 0)) (or (and (and (= (ite (= 0 (str.len value2)) 1 0) 0) true) true) (not (= (ite (str.prefixof value2 "") 1 0) 0)))) (not (= (ite (distinct key2 "a") 1 0) 0)))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 594
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/math/simplex/model_based_opt.cpp:1135

(declare-fun f (Int Int) Int)
(assert (forall ((x Int) (y Int)) (not (= (f x y) (+ (* 2 x) (* 3 y))))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 1135
!compute_def || eval(result) == eval(x)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/rewriter/poly_rewriter_def.h:686

(set-option :smt.arith.reflect false)
(declare-fun _substvar_18_ () Int)
(declare-fun i10 () Int)
(declare-fun i11 () Int)
(assert (<= 0 (- (- 0 0))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/poly_rewriter_def.h
Line: 686
num_args > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Solution soundness bug on bit-vector formula

(assert
 (exists ((s (_ BitVec 5)) )(forall ((t (_ BitVec 5)) )(not (= (bvnand s t) (bvor s (bvneg t)))))
 )
 )
(check-sat)

z3 sat.euf=true xx.smt2
sat
z3  xx.smt2
unsat

[rainoftime]

Solution soundness on real formula

(declare-fun x () Real)
(assert
 (exists ((y Real) (z Real) )(! (forall ((t Real) )(! (and (distinct x y z t) true) :qid k!3))
  :qid k!3))
 )
(check-sat)

z3 sat.euf=true tactic.default_tactic=smt xx.smt2
sat
z3  xx.smt2
unsat

[rainoftime]

src/sat/smt/euf_internalize.cpp:281

(declare-fun R_S1_V3 () Bool)
(assert (forall ((W_S1_V1 Bool)) (exists ((R_E1_V4 Bool)) (let (($x277 (forall ((V4_0 Int) (V1_0 Int) (MW_S1_V4 Bool) (E1_!16 Int) (E1_!17 Int) (S1_V1_!15 Int) (S1_V4_!12 Int)) (or W_S1_V1 (not (or (= E1_!16 E1_!17) (not (or R_S1_V3 (= V1_0 S1_V1_!15))) (and R_E1_V4 (= V4_0 (ite MW_S1_V4 S1_V4_!12 V4_0)))))))))))))
(check-sat-using (then reduce-invertible purify-arith qfufbv_ackr))

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 281
Failed to verify: s().is_external(v)

[rainoftime]

heap-use-after-free at src/sat/smt/q_mam.cpp:3708:34 in q::mam_impl::match_new_patterns()

(declare-fun P (Int) Bool)
(assert (forall ((x Int)) (or (not (P x)) (P (+ x)))))
(assert (P 1))
(assert (exists ((y Int)) (not (P 0))))
(check-sat)

[rainoftime]

Invalid model for bit-vector formula

(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(declare-fun b () (Array (_ BitVec 1) (_ BitVec 1)))
(assert (= (_ bv0 1) (select a (_ bv0 1))))
(assert (not (= a b)))
(check-sat)


z3 model_validate=true tactic.default_tactic=smt sat.euf=true xx.smt2
sat
(error "line 5 column 10: an invalid model was generated")

[rainoftime]

src/ast/euf/euf_etable.h:91

(set-option :sat.branching.heuristic chb)
(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqe) (inv) (invack))))
(declare-sort data$type)
(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort node$type)
(declare-fun shrset$1 () (Array node$type BOOL))
(declare-fun invset () (Array node$type BOOL))
(declare-fun recv_invack$i () node$type)
(declare-fun chan3$1 () (Array node$type msg$type))
(declare-fun exgntd$1 () BOOL)
(declare-fun shrset () (Array node$type BOOL))
(declare-fun chan3 () node$type)
(declare-fun curcmd () msg_cmd$type)
(assert (and (and (not (not (forall ((n node$type)) (let () (let (($x9 (= Truth (select invset n))))))))) (not (= invack (m_cmd (select chan3$1 recv_invack$i)))) (not (= curcmd empty))) (not (not (= (= shrset$1 (store shrset recv_invack$i Falsity)) (= Truth (ite (= exgntd$1 Truth) (ite (=> true (forall ((n node$type)) (! (let (($x55 true)) (=> (and (distinct (select invset n) Truth) true) (= (select shrset$1 n) Truth))) :qid k!22))) Truth Falsity) (ite (forall ((n node$type)) (! (let () (let () (=> (and (distinct (select invset n) Truth) true) (= (select shrset$1 n) Truth)))) :qid k!22)) Truth Falsity))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/euf/euf_etable.h
Line: 91
n1->get_decl() == n2->get_decl()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/ast.h:509

(declare-fun a () (Array (_ BitVec 1) (_ BitVec 1)))
(assert (exists ((b (Array (_ BitVec 1) (_ BitVec 1)))) (or (= (b (_ bv1 1)) (select a (_ bv1 1))) (not (= a b)))))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 509
m_mark1_owner == 0 || m_mark1_owner == owner
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

invalid model for array + uf

(declare-sort sko_ty_0_1793)
(declare-fun s1_1796 () (Array sko_ty_0_1793 Bool))
(declare-fun s2_1797 () (Array sko_ty_0_1793 Bool))
(declare-fun x_1795 () sko_ty_0_1793)
(assert (select ((_ map (and () Bool)) s1_1796 s2_1797) x_1795))
(assert (not (select s2_1797 x_1795)))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
sat
(error "line 7 column 10: an invalid model was generated")

[rainoftime]

invalid model for integer/real?

(assert (not (distinct 0)))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
failed to validate: (not (distinct 0))
sat
(error "line 2 column 10: an invalid model was generated")

[rainoftime]

Invalid model for floating points formula

(declare-fun X () (_ FloatingPoint 2 3))
(assert (= X (_ -oo 2 3)))
(check-sat)

z3 model_validate=true tactic.default_tactic=smt sat.euf=true delta.out.smt2
Failed to validate 8 24: (= X -oo) false
22: X
(_ +zero 2 3)
23: -oo
(_ -oo 2 3)
sat
(error "line 3 column 10: an invalid model was generated")

[NikolajBjorner]

OK, thanks. This should do for this round.

[NikolajBjorner]

stop

[NikolajBjorner]

There is per my book-keeping two unresolved bugs remaining. It is marked by a frown. The FP bug is probably a punt because there are outstanding FP bugs on the pre-existing solver and they could be duplicates.

[NikolajBjorner]

The FP bug was also fixed. According to the tests done at various times, all entered bugs are fixed. Thanks again for supplying these tests. The quality is improving, but I am sure there are still quite many bugs to weed out. If filing another batch it is easier to keep track of if it of size <= 20.