[Consolidated 2] Issues related to tactic.default_tactic=smt sat.euf=true

[rainoftime]

Invalid model

---

(declare-fun |main::i@3| () Int)
(declare-fun |main::i@4| () Int)
(declare-fun __POLICY_CHOICE_0 () Int)
(declare-fun |main::i@2| () Int)
(declare-fun __POLICY_CHOICE_2 () Int)
(declare-fun __POLICY_CHOICE_1 () Int)
(declare-fun |main::__CPAchecker_TMP_0@3| () Int)
(declare-fun __VERIFIER_nondet_bool@2 () Int)
(assert (let ((a!1 (or (and (not (<= |main::__CPAchecker_TMP_0@3| 0)) (= __POLICY_CHOICE_1 0)) (and (not (>= |main::__CPAchecker_TMP_0@3| 0)) (= __POLICY_CHOICE_1 1))))(a!2 (or (and (not (<= |main::i@2| 4)) (= __POLICY_CHOICE_2 0)) (and (not (>= |main::i@2| 4)) (= __POLICY_CHOICE_2 1))))) (and (or (and (distinct |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2) a!1 (= |main::i@2| 4) (= |main::i@3| 0) (= __POLICY_CHOICE_0 0)) (or (distinct |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2) a!1 a!2 (= |main::i@3| |main::i@2|) (= __POLICY_CHOICE_0 1))) (distinct |main::i@4| (+ 1 |main::i@3|)))))
(assert (let ((a!1 (= (- |main::i@2| 0) (* 2 (div (- |main::i@2| 0) 2))))) (and a!1 (>= |main::i@2| 0) (>= (+ (- 1) |main::i@2|) 0))))
(assert (< |main::i@4| 0))
(maximize |main::i@4|)
(check-sat)

[rainoftime]

src/sat/smt/bv_invariant.cpp:98

(set-logic QF_UFBV)
(set-option :model_validate true)
(declare-fun bv_53-0 () (_ BitVec 53))
(declare-fun bv_15-0 () (_ BitVec 15))
(minimize bv_15-0)
(maximize bv_53-0)
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
60 1 0
ASSERTION VIOLATION
File: ../src/sat/smt/bv_invariant.cpp
Line: 98
Failed to verify: _bits.size() == num_bits

[rainoftime]

src/sat/smt/euf_model.cpp:204

(set-logic QF_UFBV)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(assert (uf4 true true (= (_ bv0 44) (_ bv0 44)) true))
(check-sat)

 z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_model.cpp
Line: 204
Failed to verify: arg

---

(set-logic AUFLIRA)
(set-info :status sat)
(declare-fun f ((Array Int Bool)) Bool)
(declare-fun y () (Array Int Bool))
(assert (forall ((x (Array Int Bool))) (f y)))
(check-sat)

[rainoftime]

Nondet src/util/vector.h:484

(set-logic QF_UFBV)
(declare-fun _substvar_8_ () Bool)
(set-option :sat.threads 4)
(declare-sort S1 0)
(assert _substvar_8_)
(push 1)
(check-sat-using (then ufbv-rewriter reduce-bv-size sat-preprocess eq2bv fix-dl-var ctx-solver-simplify reduce-invertible nlsat))

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
sat
z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 484
idx < size()

Line: 484
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

ast.h:495

(set-logic QF_UFBV)
(declare-fun _substvar_45_ () Bool)
(set-option :model_validate true)
(set-option :sat.threads 4)
(assert (distinct _substvar_45_ false true (= (_ bv0 68) (_ bv0 68) (_ bv0 68) (_ bv0 68) (_ bv0 68))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
unsat
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 495
m_ref_count > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Memory leak

(set-logic QF_UFBV)
(declare-fun _substvar_41_ () (_ BitVec 3))
(declare-fun _substvar_62_ () (_ BitVec 3))
(declare-fun v6 () Bool)
(declare-fun bv_3-0 () (_ BitVec 3))
(assert (or (= _substvar_62_ bv_3-0 _substvar_41_ (_ bv0 3)) (= (= (_ bv0 3) bv_3-0 (bvsdiv bv_3-0 bv_3-0) (_ bv0 3)) v6 true true true)))
(check-sat)

---

(declare-fun X () (_ FloatingPoint 2 6))
(declare-fun Y () (_ FloatingPoint 2 6))
(declare-fun Z () (_ FloatingPoint 2 6))
(declare-fun W () (_ FloatingPoint 2 6))
(assert (and (distinct X (fp.mul RTZ Y Z)) (distinct X (fp.sub RTZ Y Z)) (= X (fp.div RTZ Y Z)) (= X (fp.add RTZ Y Z)) (= X (fp.fma RTZ Y Z W)) (= X (fp.sqrt RTZ Y)) (distinct X (fp.rem X Y)) (distinct X (fp.roundToIntegral RTZ Y)) (distinct X (fp.max Y Z)) (distinct X (fp.min Y Z))))
(check-sat)

(set-logic QF_AUFLIA)
(declare-fun _substvar_508_ () Int)
(declare-fun ALU (Int Int Int) Int)
(assert (not (= (ALU 0 0 0) (ALU 0 (ite false 0 _substvar_508_) 0))))
(check-sat)

A stack with allocation locations would be greatly appreciated.

[rainoftime]

src/sat/smt/bv_invariant.cpp:103

(set-logic QF_UFBV)
(set-option :model_validate true)
(declare-fun bv_51-0 () (_ BitVec 51))
(maximize bv_51-0)
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/bv_invariant.cpp
Line: 103
bits[zo.m_is_true][zo.m_idx]
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Nondet src/math/lp/lar_solver.cpp:1183

(set-logic QF_LIA)
(set-option :sat.threads 4)
(assert (< 18 0))
(check-sat)

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

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
false l_undef 24: (< 18 0)
1 l_undef l_true 24: (< 18 0)
0  <= v4
updates 13
newlits 0 qhead: 0
neweqs  0 qhead: 0
#27 := 1 [t 5:0] 
#28 := 1.0 [t 5:1] 
#23 := 0 [t 5:2] 
#29 := 0.0 [t 5:3] 
#24 := (< 18 0) [t 5:5] 
#22 := 18 [t 5:4] 
bool-vars
1: 24 l_true (< 18 0)
number of constraints = 12
(0) j0 >= 1
(1) j0 <= 1
(2) j1 >= 1
...
File: ../src/math/lp/lar_solver.cpp
Line: 1183
get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/euf/euf_egraph.cpp:294

(set-logic AUFLIA)
(declare-fun datai__first () Int)
(declare-fun a.select (Int Int) Int)
(assert (forall ((?I Int)) (<= datai__first (a.select 0 ?I))))
(check-sat)
(exit)

z3 tactic.default_tactic=smt sat.euf=true yy.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 294
NOT IMPLEMENTED YET!
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/euf_solver.cpp:367

(set-option :sat.euf true)
(declare-fun uf3_2 (Bool Bool Bool) Bool)
(declare-fun v3 () Bool)
(declare-fun v8 () Bool)
(declare-fun v15 () Bool)
(declare-fun v17 () Bool)
(assert-soft (xor v3 true (uf3_2 v8 v15 false)) :weight 1)
(assert-soft (uf3_2 false false false) :weight 1)
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/euf_solver.cpp
Line: 367
val != l_undef
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

As I wrote in the other bug: please don't file yet with :sat.threads or parallel.enable. These bugs often already manifest without threads, and if they only manifest with threads they are harder to debug. There is a different time to worry about multi-threaded behavior for the new code (the bugs would be around how constraints are copied).

[NikolajBjorner]

Threads are now disabled when using euf

[NikolajBjorner]

(set-option :model_validate true)
(set-option :sat.threads 2)
(declare-fun bv_2-0 () (_ BitVec 2))
(assert (= bv_2-0 (bvnand bv_2-0 (_ bv1 2))))
(check-sat-using uflra)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
Failed to validate 38: (not (bit2bool[0] bv_2-0)) true
Failed to validate 35: (= bv_2-0 (concat bv[1:1] (bvnot #29))) false
22: bv_2-0
#b00
34: (concat bv[1:1] (bvnot (extract[0:0] bv_2-0)))
#b11
sat
(error "line 5 column 22: an invalid model was generated")

Commit 0422b59

[rainoftime]

(assert
 (let (($x11 (forall ((x (_ BitVec 4)) )(! (forall ((y (_ BitVec 4)) )(! (= (bvadd x y) (_ bv0 4)) :qid k!5))
  :qid k!5))
 ))
 (let (($x22 (or $x11)))
 (let (($x17 (and $x11)))
 (and $x22 $x17 $x22 $x22 $x22 $x22 $x17 $x17 $x17 $x22 $x17 $x22 $x17 $x17 $x22 $x22 $x17 $x17 $x22 $x22 $x22 $x17 $x22 $x22 $x17 $x17 $x17 $x22 $x22 $x17 $x22 $x22 $x17 $x17 $x17 $x17 $x17 $x17 $x22 $x22 $x22 $x17 $x22)))))
(check-sat)

 File: ../src/sat/smt/bv_internalize.cpp
 Line: 287
 s().value(m_bits[v][idx]) != l_undef
 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

(assert
 (forall ((v1 Real) )(exists ((v0 Real) )(and (= (+ 1.0 v0 v1) v0)))
 )
 )
(check-sat)

 File: ../src/ast/rewriter/expr_safe_replace.cpp
 Line: 27
 src->get_sort() == dst->get_sort()
 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

All bugs marked by "eyes" are addressed.
The first one uses optimization (maximize).
To keep it focused, optimization is not going to be supported in a first round with the new core.