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

[rainoftime]

Hi, for the following formula,
z3 f91c3d9

(set-option :sat.branching.heuristic chb)
(assert (forall ((arr (Array Bool Int))) (forall ((i10 Int)) (exists ((v18 Bool)) (and (= i10 1) (> (select (store arr v18 1) false) 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]

sat/smt/sat_dual_solver.cpp:149

(set-option :sat.branching.heuristic chb)
(set-option :rewriter.elim_and true)
(declare-fun x6 () Bool)
(declare-fun x8 () Bool)
(declare-fun x1 () (_ BitVec 16))
(declare-fun x2 () (_ BitVec 16))
(declare-fun x3 () Bool)
(assert (forall ((x4 Bool)) (exists ((x7 Bool)) (forall ((x10 (_ BitVec 16))) (and x3 x4 x8 x6 (bvslt (_ bv1 16) (bvadd x10 (bvsub x2 x1))) (bvslt (_ bv0 16) (bvadd (bvsub (_ bv0 16) (bvsub x2 x1)) x10)))))))
(check-sat)

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

[rainoftime]

SEGV ../src/ast/euf/euf_enode.h:192

(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort process$type)
(declare-fun valid () (Array resource$type BOOL))
(declare-fun S$cardinality (S$t$type) Int)
(assert (forall ((S$empty S$t$type)) (exists ((ref$1 (Array process$type resource$type))) (forall ((ref (Array process$type resource$type))) (let (($x203 ref$1)) (and (= 0 (S$cardinality S$empty)) (not (or (not (forall ((p process$type)) (let (($x171 (= Truth (select valid (ref p)))))))) (forall ((p process$type)) (let (($x182 (= Truth (select valid (ref$1 p)))))))))))))))
(check-sat)

[rainoftime]

"failed to verify" and leak (needs the option model_validate)

(set-option :rewriter.expand_nested_stores true)
(declare-datatypes ((BOOL 0)) (((Truth))))
(declare-sort data$type)
(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))))
(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-sort node$type)
(declare-fun shrset () (Array node$type BOOL))
(assert (exists ((auxdata$1 data$type)) (exists ((store_data$i node$type)) (exists ((cache (Array node$type cache$type))) (forall ((store_data$d data$type)) (exists ((cache$1 (Array node$type cache$type))) (and (= auxdata$1 store_data$d) (forall ((n node$type)) (= Truth (select shrset n))) (= cache$1 (store cache store_data$i (c_cache$type (c_state (cache store_data$i)) store_data$d))) (not (forall ((n node$type)) (= invalid (c_state (cache$1 n))))))))))))
(check-sat)

[rainoftime]

at cf9e55f

(set-option :rewriter.eq2ineq true)
(declare-sort us_main_type)
(declare-datatypes ((us_rep2 0)) (((us_repqtmk2 (rec__test_route__route_acc__is_null_pointer Bool) (rec__test_route__route_acc__pointer_address Int) (rec__test_route__route_acc__pointer_value_abstr us_main_type)))))
(declare-datatypes ((us_split_fields2 0)) (((us_split_fieldsqtmk1 (rec__test_route__route__rest us_rep2)))))
(declare-datatypes ((us_rep3 0)) (((us_repqtmk3 (us_split_fields3 us_split_fields2)))))
(declare-fun length (us_rep2) Int)
(declare-fun us_close (us_rep3) us_main_type)
(declare-fun r__pointer_value () us_split_fields2)
(declare-fun temp___borrowed_250 () us_rep2)
(assert (exists ((r__is_null_pointer Bool)) (forall ((r__pointer_address Int)) (and (not (= (length temp___borrowed_250) (length (us_repqtmk2 r__is_null_pointer r__pointer_address (us_close (us_repqtmk3 r__pointer_value)))))) (forall ((temp___borrowed_236 us_rep2)) (let (($x149 (= (length temp___borrowed_236) (length (us_repqtmk2 r__is_null_pointer r__pointer_address (us_close (us_repqtmk3 r__pointer_value)))))))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

heap-use-after-free at /sat/smt/euf_solver.cpp:492

(declare-sort u2)
(declare-fun y () Bool)
(assert (exists ((yw u2)) (let (($x23 y)))))
(check-sat)

This is a regression introduced when fixing a different bug. It should crash elsewhere too (but requires that the benchmark doesn't introduce "true"/"false" early on). Anyhow, it is fixed so better use the new bits.

[NikolajBjorner]

The ""failed to verify" and leak (needs the option model_validate)" bug is likely to take more time to debug. Other bugs are easier/more self-contained so makes sense to upload more on this thread since the one remaining bug could be sitting there a little.

[rainoftime]

at 9e306e3
invalid model (maybe related to unfixed one)
this can be triggered without tactic.default_tactic=smt sat.euf=true

(set-option :model_validate true)
(set-option :rewriter.expand_nested_stores true)
(declare-fun a () (Array Bool Int))
(declare-fun r () (Array (Array Bool Int) Int))
(assert-soft false)
(assert (= (select a false) (- (select a false) (select a false) (select r (store a false (select a true))))))
(check-sat)

This is unrelated to sat.euf.
Since it happens for optimization where you are using some non-standard parameter I have to give this very low priority and therefore punt on it.

[rainoftime]

/src/util/vector.h:474

(set-logic QF_BV)
(declare-fun v9 () Bool)
(push 2)
(assert false)
(push 5)
(assert v9)
(push 2)
(pop 8)
(assert false)
(push)

[rainoftime]

src/sat/smt/q_mam.cpp:932

(set-option :rewriter.elim_and true)
(declare-sort us_main_type)
(declare-datatypes ((us_rep2 0)) (((us_repqtmk2 (rec__test_route__route_acc__is_null_pointer Bool) (rec__test_route__route_acc__pointer_address Int) (rec__test_route__route_acc__pointer_value_abstr us_main_type)))))
(declare-datatypes ((us_rep1 0)) (((us_repqtmk1 (rec__test_route__point_acc__is_null_pointer Bool)))))
(declare-datatypes ((us_split_fields2 0)) (((us_split_fieldsqtmk1 (rec__test_route__route__rest us_rep2)))))
(declare-datatypes ((us_rep3 0)) (((us_repqtmk3 (us_split_fields3 us_split_fields2)))))
(declare-sort us_pledge_ty)
(declare-fun length (us_rep2) Int)
(declare-fun us_close (us_rep3) us_main_type)
(declare-fun r__pointer_value () us_split_fields2)
(declare-fun us_pledge_get (us_pledge_ty us_rep2 us_rep1) Bool)
(declare-fun test_route__nth_point__pledge (us_rep2 Int) us_pledge_ty)
(assert (exists ((us_null_pointer us_rep1)) (forall ((r__is_null_pointer Bool)) (forall ((r__pointer_address Int)) (exists ((temp___borrowed_250 us_rep2)) (and true (rec__test_route__point_acc__is_null_pointer us_null_pointer) (= (length temp___borrowed_250) (length (us_repqtmk2 r__is_null_pointer r__pointer_address (us_close (us_repqtmk3 r__pointer_value))))) (forall ((temp___borrowed_236 us_rep2)) (forall ((temp___brower_235 us_rep1)) (or (= (length temp___borrowed_236) (length (us_repqtmk2 r__is_null_pointer r__pointer_address (us_close (us_repqtmk3 r__pointer_value))))) (and (rec__test_route__point_acc__is_null_pointer temp___brower_235) (us_pledge_get (test_route__nth_point__pledge (us_repqtmk2 r__is_null_pointer r__pointer_address (us_close (us_repqtmk3 r__pointer_value))) 1) temp___borrowed_236 temp___brower_235)))))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 932
!is_quantifier(p)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB