[consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778

rainoftime · 2022-01-17T02:45:31Z

Hi, for the following formula,
z3 637ddf9

(declare-fun c () (Array (_ BitVec 2) (_ BitVec 1)))
(assert (forall ((b (Array (_ BitVec 2) (_ BitVec 1)))) (exists ((ag (_ BitVec 1))) (forall ((a (_ BitVec 2))) (exists ((ak (_ BitVec 2))) (and (= a ((_ zero_extend 1) (b (_ bv0 2)))) (= (_ bv1 1) (ite (not (= (_ bv0 1) (select c a))) (_ bv1 1) (_ bv0 1))) (= (_ bv1 1) (ite (= b (store (store c (bvnand a (_ bv1 2)) ag) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1)))))))))
(check-sat-using bv)

ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 172
m_egraph.find(e)->bool_var() == v
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

The text was updated successfully, but these errors were encountered:

rainoftime · 2022-01-17T02:54:27Z

src/sat/smt/arith_solver.cpp:616

(assert (forall ((x Real)) (exists ((y Real)) (and (not (= 0.0 y)) (not (= 0.0 (+ y (sin x))))))))
(check-sat)

v5 j4 = 0 := #58: x!1
v6 t6 = -1 := #77: (+ x!1 (sin x!1))
v7 7 l_true := #67: (<= (sin x!1) -1.0)
(define-fun x!1 () Real
  0.0)

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

rainoftime · 2022-01-17T03:25:31Z

/src/util/vector.h:474

(set-option :sat.branching.heuristic chb)
(set-option :rewriter.push_ite_arith true)
(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort process$type)
(declare-fun ref () (Array process$type resource$type))
(declare-fun S$empty () S$t$type)
(declare-fun handles () (Array resource$type S$t$type))
(declare-fun count () (Array resource$type Int))
(declare-fun count$1 () (Array resource$type Int))
(declare-fun S$cardinality (S$t$type) Int)
(declare-fun S$mem (process$type S$t$type) BOOL)
(declare-fun S$remove (process$type S$t$type) S$t$type)
(declare-fun S$add (process$type S$t$type) S$t$type)
(assert (forall ((create$r resource$type)) (forall ((valid$1 (Array resource$type BOOL))) (forall ((valid (Array resource$type BOOL))) (forall 
((handles$1 (Array resource$type S$t$type))) (exists ((null resource$type)) (and (forall ((e process$type)) (not (= Truth (S$mem e S$empty)))) 
(forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$add y s)) Truth)) (forall ((x process$type) (y process$type) (s S$t$typ
e)) (= (S$mem x (S$remove y s)) (ite (and (not (= x y)) (and (distinct (S$mem x s) Truth))) Truth Falsity))) (and (distinct (S$cardinality S$em
pty) 0)) (forall ((s S$t$type)) (=> (= (S$cardinality s) 0) (= s S$empty))) (forall ((s S$t$type)) (>= (S$cardinality s) 0)) (forall ((x proces
s$type) (s S$t$type)) (= (S$cardinality (S$add x s)) (ite (= (S$mem x s) Truth) (S$cardinality s) (+ 1 (S$cardinality s))))) (not (=> (and (not
 (= create$r null)) (= valid$1 (store valid create$r Truth)) (= count$1 (store count create$r 0)) (= handles$1 (store handles create$r S$empty)
) (not (= (valid create$r) Truth)) (and (forall ((p process$type)) (=> (not (= (select ref p) null)) (= (valid (select ref p)) Truth))) (forall
 ((p process$type)) (=> (not (= (select ref p) null)) (> (select count (select ref p)) 0))))) (forall ((p process$type)) (=> (not (= (select re
f p) null)) (= (valid$1 (select ref p)) Truth))))))))))))
(check-sat)
(check-sat-using (then simplify nnf ufbv))

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

rainoftime · 2022-01-17T03:35:27Z

(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort node$type)
(assert (forall ((shrset (Array node$type BOOL))) (exists ((shrset$1 (Array node$type BOOL))) (and (= shrset$1 shrset) (= Truth (ite true Falsity (ite (forall ((n node$type)) (let (($x140 (= (shrset$1 n) Truth))))) Truth Falsity)))))))
(check-sat-using (then nnf qfnia))

ASSERTION VIOLATION
File: ../src/sat/sat_gc.cpp
Line: 479
lvl(lit) == 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

zhendongsu · 2022-01-17T14:41:09Z

[513] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
false l_true 140: (<= 1/2 (select (t #23 1/2) 0))
...
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 618
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[514] % 
c[514] % cat small.smt2 
(declare-fun d (Int Int) Int)
(declare-fun t ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun t (Int Real) (Array Int Real))
(assert (forall ((V Real)) (= V (select (t (d 0 0) V) 0))))
(assert (exists ((B (Array Int (Array Int Real)))) (= (select (select (t B) 0) 0) (select (select (t B) 0) 1))))
(assert (forall ((D (Array Int (Array Int Real)))) (= (select (D 0) 0) (select (D 1) 0))))
(check-sat)

merlinsun · 2022-01-19T02:25:34Z

memory leaks

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unknown

=================================================================
==3401337==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 64 byte(s) in 1 object(s) allocated from:
    #0 0x7fc6d2eeebc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x55bcb948c656 in memory::allocate(unsigned long) (/z3/build/z3+0x662f656)
    #2 0x55bcb62a74a6 in q::ematch::clausify(quantifier*) (/z3/build/z3+0x344a4a6)
    #3 0x55bcb62a9f92 in q::ematch::add(quantifier*) (/z3/build/z3+0x344cf92)
    #4 0x55bcb6157a2e in q::solver::asserted(sat::literal) (/z3/build/z3+0x32faa2e)
    #5 0x55bcb5f3d16e in euf::solver::asserted(sat::literal) (/z3/build/z3+0x30e016e)
    #6 0x55bcb86f20c6 in sat::solver::propagate_literal(sat::literal, bool) (/z3/build/z3+0x58950c6)
    #7 0x55bcb86f53cd in sat::solver::propagate_core(bool) (/z3/build/z3+0x58983cd)
    #8 0x55bcb86f9bdd in sat::solver::propagate(bool) [clone .constprop.0] (/z3/build/z3+0x589cbdd)
    #9 0x55bcb8736bde in sat::solver::check(unsigned int, sat::literal const*) (/z3/build/z3+0x58d9bde)
    #10 0x55bcb5f34b26 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/z3/build/z3+0x30d7b26)
    #11 0x55bcb5f3a074 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/z3/build/z3+0x30dd074)
    #12 0x55bcb7346b48 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/z3/build/z3+0x44e9b48)
    #13 0x55bcb736d4f9 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/z3/build/z3+0x45104f9)
    #14 0x55bcb736ff46 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/z3/build/z3+0x4512f46)
    #15 0x55bcb7197889 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/z3/build/z3+0x433a889)
    #16 0x55bcb712e4be in solver_na2as::check_sat_core(unsigned int, expr* const*) (/z3/build/z3+0x42d14be)
    #17 0x55bcb714fb54 in combined_solver::check_sat_core(unsigned int, expr* const*) (/z3/build/z3+0x42f2b54)
    #18 0x55bcb716eb27 in solver::check_sat(unsigned int, expr* const*) (/z3/build/z3+0x4311b27)
    #19 0x55bcb70c8615 in cmd_context::check_sat(unsigned int, expr* const*) (/z3/build/z3+0x426b615)
    #20 0x55bcb6fd8798 in smt2::parser::operator()() (/z3/build/z3+0x417b798)
    #21 0x55bcb6f69ff1 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/z3/build/z3+0x410cff1)
    #22 0x55bcb363552a in read_smtlib2_commands(char const*) (/z3/build/z3+0x7d852a)
    #23 0x55bcb357efda in main (/z3/build/z3+0x721fda)
    #24 0x7fc6d28a70b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x270b2)

Indirect leak of 96 byte(s) in 1 object(s) allocated from:
    #0 0x7fc6d2eeebc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x55bcb948c656 in memory::allocate(unsigned long) (/z3/build/z3+0x662f656)
    #2 0x55bcb62a8ac9 in q::ematch::clausify(quantifier*) (/z3/build/z3+0x344bac9)
    #3 0x55bcb62a9f92 in q::ematch::add(quantifier*) (/z3/build/z3+0x344cf92)
......
SUMMARY: AddressSanitizer: 160 byte(s) leaked in 2 allocation(s).
$ cat delta.smt2 
(declare-fun v () Bool)
(assert (forall ((T Bool)) (xor v T (and v (not (xor false))))))
(check-sat)

zhendongsu · 2022-01-19T07:58:17Z

Might be related to #5778 (comment):

[513] % z3debug model_evaluator.array_equalities=false tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
[514] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
...
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 618
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[515] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(declare-fun a1 () (Array Int Int))
(declare-fun a2 ((Array Int Int) (Array Int Int)) Int)
(assert (let ((v0 a1) (v1 (store (store a1 0 0) 1 0))) (distinct (v0 (a2 a1 v1)) (v1 (a2 a1 a1)))))
(check-sat)

merlinsun · 2022-01-21T03:23:45Z

invalid model

$ z3 tactic.default_tactic=smt sat.euf=true model_validate=true delta.smt2
sat
(error "line 2 column 40: an invalid model was generated")
(
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    0)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 0) (= x!1 0)) (- 1)
      0))
)

$ cat delta.smt2
(assert (distinct true (= 0 (rem 0 0))))
(check-sat-using (then purify-arith sat))
(get-model)

zhendongsu · 2022-01-21T10:08:11Z

[514] % z3release model_validate=true small.smt2
sat
[515] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (let ((a!1 (= t!4
              (r #b00
                 (store ((as const (Array (_ BitVec 2) (_ BitVec 2))) #b11)
                        #b00
                        #b00))))
      (a!2 (ite (bvsle (select (conte t!4) k!5) #b00)
                (r #b00 (_ as-array k!0))
                t!4)))
(let ((a!3 (= a!2
              (r #b00
                 (store ((as const (Array (_ BitVec 2) (_ BitVec 2))) #b11)
                        #b00
                        #b00)))))
  (not (or (bvsle #b00 (s t!4)) a!1 (not a!3)))))
evaluated to false
...
[516] % 
[516] % cat small.smt2
(declare-const x Bool)
(declare-datatypes ((r 0)) (((r (s (_ BitVec 2)) (conte (Array (_ BitVec 2) (_ BitVec 2)))))))
(declare-fun i (r (_ BitVec 2)) Bool)
(declare-fun r ((_ BitVec 2) r (_ BitVec 2)) Bool)
(declare-fun e () r)
(assert (forall ((s (_ BitVec 2))) (= (i e (_ bv0 2)) (r (_ bv0 2) e (_ bv0 2)))))
(assert (forall ((s (_ BitVec 2))) (= true (r (_ bv0 2) e (_ bv0 2)))))
(assert (forall ((t r) (k (_ BitVec 2))) (or (not (i t k)) (bvsge (s t) (_ bv0 2)) (i (ite (bvsge (_ bv0 2) (select (conte t) k)) (ite x (r (s t) (store (conte t) (_ bv0 2) (bvnot (select (conte t) (_ bv0 2))))) e) t) (_ bv0 2)))))
(check-sat)

zhendongsu · 2022-01-21T10:09:57Z

[509] % z3release model_validate=true small.smt2
sat
[510] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
[511] % 
[511] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(declare-fun a1 () (Array Int Int))
(declare-fun a2 () (Array Int Int))
(declare-fun s ((Array Int Int) (Array Int Int)) Int)
(assert (distinct a2 a1))
(assert (= 1 (select a2 0)))
(assert (distinct 0 (s a2 (store a1 0 0))))
(check-sat)

zhendongsu · 2022-01-21T18:15:43Z

[570] % z3release model_validate=true small.smt2 
sat
[571] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 19 200: (<= (select (select a!13 #139) (array-ext[0] #140 #150)) 0.0) false
...
[572] % 
[572] % cat small.smt2 
(declare-fun t ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun t ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((N Int) (a (Array Int (Array Int Real)))) (= (select (select (t a) 1) 0) (select (select (t a) 0) 0))))
(assert (forall ((b Int)) true))
(assert (exists ((x0 Int) (x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (D (Array Int (Array Int Real))) (E (Array Int (Array Int Real)))) (not (= (select (select (t D) 2) 0) (select (select (t (t (t D) (t E))) 1) 0)))))
(check-sat)

zhendongsu · 2022-01-21T18:38:04Z

[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
missed propagation 0
missed propagation 1
Failed to validate 192 1512: (<= (+ x!2 (* -1 y!3)) 0) false
...
[512] % 
[512] % cat small.smt2
(declare-fun Sm () Int)
(declare-fun r (Int Int) Int)
(assert (forall ((x Int) (y Int)) (= (= x y) (= Sm (r x y)))))
(check-sat)

zhendongsu · 2022-01-22T08:53:14Z

Solution unsoundness:

[518] % cp out.smt2 small.smt2
[519] % z3release rewriter.sort_sums=true rewriter.arith_lhs=true tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[520] % z3release rewriter.sort_sums=true rewriter.arith_lhs=true small.smt2
unsat
[521] % z3release small.smt2
unsat
[522] % cat small.smt2
(assert (forall ((a Int) (b Int)) (= a b)))
(check-sat)

not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.

zhendongsu · 2022-01-23T16:33:53Z

Invalid model:

[528] % z3release model_validate=true small.smt2
sat
[529] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 13 column 30: an invalid model was generated")
[530] % cat small.smt2
(declare-sort U)
(declare-sort R)
(declare-fun r () R)
(declare-fun s () R)
(declare-fun o () R)
(declare-fun m (R R) Bool)
(declare-fun a (U Real) Bool)
(assert (exists ((u U) (v Real)) (and (a u v) (a u 0.0))))
(assert (exists ((t R)) (and (m t s) (or (m s t) (m s s)))))
(assert (forall ((r R)) (m o r)))
(assert (m s r))
(assert (forall ((Z R)) (m Z r)))
(check-sat-using (then bv smt))

zhendongsu · 2022-01-26T10:56:42Z

[527] % z3release model_validate=true small.smt2
sat
[528] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 5 column 61: an invalid model was generated")
[529] % 
[529] % cat small.smt2
(declare-const a (_ BitVec 1))
(declare-const b (Array (_ BitVec 32) (_ BitVec 8)))
(assert (distinct ((_ zero_extend 7) a) (select b (_ bv1 32))))
(assert (= a (ite (= b (store b (_ bv0 32) (_ bv1 8))) (_ bv1 1) (_ bv0 1))))
(check-sat-using (then ctx-solver-simplify bit-blast qfaufbv))

zhendongsu · 2022-01-27T12:07:48Z

A simpler instance than #5778 (comment):

[570] % z3release model_validate=true small.smt2
sat
[571] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 5 column 10: an invalid model was generated")
[572] % 
[572] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(assert (= a (store b 1 1)))
(check-sat)

merlinsun · 2022-02-05T07:55:48Z

$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
Failed to validate 3 35: (= a (store v 1 (store #26 0 #27))) false
......
$ cat delta.smt2
(declare-fun v () (Array Int (Array Int Real)))
(declare-fun a () (Array Int (Array Int Real)))
(assert (or true (distinct a (store v 1 (store (select v 0) 0 0)) a)))
(check-sat)

z3 4749495

merlinsun · 2022-02-18T10:49:43Z

$ z3debug tactic.default_tactic=smt sat.euf=true case.smt2
Failed to validate 8 76: (= (^ 0.0 0.0) (array-ext[0] v (store #31 #33 #27))) false
......
==21442==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 8 byte(s) in 1 object(s) allocated from:
    #0 0x7f1983d76b40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40)
    #1 0x55b48c2d89a3 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55b48c34445d in region::allocate(unsigned long) ../src/util/region.cpp:28
    #3 0x55b489ff70dc in operator new[](unsigned long, region&) ../src/util/region.h:93
    #4 0x55b489ff57fe in smt::ext_simple_justification::ext_simple_justification(region&, unsigned int, sat::literal const*, unsigned int, std::pair<smt::enode*, smt::enode*> const*) ../src/smt/smt_justification.cpp:305
    #5 0x55b489cafb07 in smt::ext_theory_simple_justification::ext_theory_simple_justification(int, region&, unsigned int, sat::literal const*, unsigned int, std::pair<smt::enode*, smt::enode*> const*, unsigned int, parameter*) (/root/z3debug/build/z3+0x11e7b07)
    #6 0x55b489cafe78 in smt::ext_theory_eq_propagation_justification::ext_theory_eq_propagation_justification(int, region&, unsigned int, sat::literal const*, unsigned int, std::pair<smt::enode*, smt::enode*> const*, smt::enode*, smt::enode*, unsigned int, parameter*) ../src/smt/smt_justification.h:374
    #7 0x55b48a484fcc in smt::theory_lra::imp::assign_eq(int, int) ../src/smt/theory_lra.cpp:3039
    #8 0x55b48a47bf85 in smt::theory_lra::imp::add_eq(unsigned int, unsigned int, lp::explanation const&, bool) (/root/z3debug/build/z3+0x19b3f85)
    #9 0x55b48a49cd23 in lp::lp_bound_propagator<smt::theory_lra::imp>::add_eq_on_columns(lp::explanation const&, unsigned int, unsigned int, bool) ../src/math/lp/lp_bound_propagator.h:580
    #10 0x55b48a4950c0 in lp::lp_bound_propagator<smt::theory_lra::imp>::try_add_equation_with_lp_fixed_tables(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>::vertex const*) ../src/math/lp/lp_bound_propagator.h:176
    #11 0x55b48a49ebdb in lp::lp_bound_propagator<smt::theory_lra::imp>::try_add_equation_with_fixed_tables(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>::vertex const*) ../src/math/lp/lp_bound_propagator.h:679
    #12 0x55b48a49ecf9 in lp::lp_bound_propagator<smt::theory_lra::imp>::handle_fixed_phase(unsigned int) ../src/math/lp/lp_bound_propagator.h:687
    #13 0x55b48a49f4cf in lp::lp_bound_propagator<smt::theory_lra::imp>::cheap_eq_tree(unsigned int) ../src/math/lp/lp_bound_propagator.h:704
    #14 0x55b48a4a0efe in void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&) ../src/math/lp/lar_solver.h:379
    #15 0x55b48a478f3c in smt::theory_lra::imp::propagate_bounds_with_lp_solver() (/root/z3debug/build/z3+0x19b0f3c)
    #16 0x55b48a478d82 in smt::theory_lra::imp::propagate_core() (/root/z3debug/build/z3+0x19b0d82)
    #17 0x55b48a47814d in smt::theory_lra::imp::propagate() (/root/z3debug/build/z3+0x19b014d)
    #18 0x55b48a446b6c in smt::theory_lra::propagate() ../src/smt/theory_lra.cpp:3826
    #19 0x55b489f66d2b in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1624
    #20 0x55b489f680e7 in smt::context::propagate() ../src/smt/smt_context.cpp:1712
    #21 0x55b489f88c30 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3820
    #22 0x55b489f86b56 in smt::context::search() ../src/smt/smt_context.cpp:3705
    #23 0x55b489f84a61 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3588
    #24 0x55b48a128246 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:128
    #25 0x55b489ff9b44 in check_sat_core2 ../src/smt/smt_solver.cpp:200
    #26 0x55b48b1f8d7e in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #27 0x55b48b21fb4a in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:225
    #28 0x55b48b2141d1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #29 0x55b48b18f5e1 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702

SUMMARY: AddressSanitizer: 8 byte(s) leaked in 1 allocation(s).
$ z3release tactic.default_tactic=smt sat.euf=true case.smt2
Failed to validate 8 76: (= (^ 0.0 0.0) (array-ext[0] v (store #31 #33 #27))) false
......
$ cat case.smt2
(declare-fun v () (Array Real Real))
(declare-fun a () Int)
(push)
(assert (distinct v (store (store (store v 0.0 (^ 0.0 0.0)) (^ 0.0 0.0) (to_real a)) 2 (^ 0.0 0.0))))
(check-sat)

NB: The use of (^ 0.0 0.0) is somewhat parthological. Not too interesting to consider at this point.
Self-validation and model reconstruction for ^ could maybe adapted, but is mostly busy-work.

zhendongsu · 2022-03-20T17:16:10Z

Refutation unsoundness:

[540] % z3release model_validate=true small.smt2
sat
[541] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[542] % cat small.smt2
(define-sort a () Int)
(define-sort b () (Set a))
(declare-fun c (Int) b)
(declare-fun d () Int)
(declare-fun f () Int)
(declare-fun g () b)
(declare-fun e () b)
(assert (= (c d) (setminus g e) (union e (c f))))
(assert (or (distinct (c f) (setminus e (c f)))))
(check-sat-using default)

zhendongsu · 2022-03-20T20:54:52Z

Assertion violation with the debug build (not an easy reduction, and the reduced formula causes an error, although the original does not):

[526] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
(error "line 4 column 54: invalid assert command, term is not Boolean")
sat
sat
sat
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[527] % cat small.smt2
(declare-fun x0 () (Array (_ BitVec 32) (_ BitVec 8)))

(assert (let ((a (concat (_ bv1 2)))) (fp (_ bv1 1) (_ bv0 11)
  (_ bv0 2)) (concat (_ bv0 32) (_ bv7 2) (_ bv3 32))))

(assert (let ((b (concat (select x0 (_ bv0 32))))) (fp.leq ((_ to_fp
  11 53) (concat (select x0 (_ bv23 32)) (select x0 (_ bv22 32))
  (select x0 (_ bv21 32)) (select x0 (_ bv10 32)) (select x0 (_ bv19
  32)) (select x0 (_ bv18 32)) (select x0 (_ bv0 32)) (select x0 (_
  bv8 32)))) ((_ to_fp 11 53) (concat (select x0 (_ bv3 32)) (select
  x0 (_ bv6 32)) (select x0 (_ bv0 32)) (select x0 (_ bv0 32)) (select
  x0 (_ bv3 32)) (concat (select x0 (_ bv2 32)) (select x0 (_ bv1 32))
  (select x0 (_ bv0 32))))))))

(assert (fp.isNegative ((_ to_fp 11 53) (concat (select x0 (_ bv23
  32)) (concat (select x0 (_ bv22 32)) (select x0 (_ bv21 32)) (concat
  (select x0 (_ bv20 32)) (select x0 (_ bv19 32)) (concat (select x0
  (_ bv18 32)) (concat (select x0 (_ bv17 32)) (select x0 (_ bv8
  32)))))))))) (check-sat-using (then purify-arith qe2 bv))

(check-sat-using (then purify-arith qe2 lia))

(assert (let ((c (fp (_ bv0 1) (_ bv0 11) (_ bv0 2)))) (or (fp.isNaN
  ((_ to_fp 11 53) (concat (select x0 (_ bv39 32)) (concat (select x0
  (_ bv4 32)) (concat (select x0 (_ bv37 32)) (concat (select x0 (_
  bv36 32)) (concat (select x0 (_ bv35 32)) (concat (select x0 (_ bv34
  32)) (concat (select x0 (_ bv33 32)) (select x0 (_ bv32
  32))))))))))) (fp.geq ((_ to_fp 11 53) (concat (select x0 (_ bv39
  32)) (concat (select x0 (_ bv4 32)) (concat (select x0 (_ bv37 32))
  (concat (select x0 (_ bv36 32)) (concat (select x0 (_ bv35 32))
  (concat (select x0 (_ bv34 32)) (concat (select x0 (_ bv33 32))
  (select x0 (_ bv32 32)))))))))) ((_ to_fp 11 53) (concat (select x0
  (_ bv23 32)) (concat (select x0 (_ bv22 32)) (select x0 (_ bv21 32))
  (concat (select x0 (_ bv20 32)) (select x0 (_ bv19 32)) (select x0
  (_ bv18 32)) (concat (select x0 (_ bv17 32)) (select x0 (_ bv8
  32)))))))))))

(check-sat-using (then purify-arith qe2 lia))

(assert (fp.leq ((_ to_fp 11 53) (concat (select x0 (_ bv39 32))
  (concat (select x0 (_ bv4 32)) (concat (select x0 (_ bv37 32))
  (concat (select x0 (_ bv36 32)) (concat (select x0 (_ bv35 32))
  (concat (select x0 (_ bv34 32)) (concat (select x0 (_ bv33 32))
  (select x0 (_ bv32 32)))))))))) ((_ to_fp 11 53) (concat (select x0
  (_ bv3 32)) (concat (select x0 (_ bv1 32)) (concat (select x0 (_ bv5
  32)) (concat (select x0 (_ bv4 32)) (concat (select x0 (_ bv0 32))
  (concat (select x0 (_ bv2 32)) (select x0 (_ bv1 32)) (select x0 (_
  bv0 32)))))))))))

(check-sat-using (then purify-arith qe2 lia))

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

merlinsun · 2022-03-22T07:06:22Z

Assertion violation
It may have just been introduced because it doesn't appear in 00608cd.

$ z3-debug tactic.default_tactic=smt sat.euf=true delta.smt2
num-conflicts: 4
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 2537
Failed to verify: idx > 0

$ z3release tactic.default_tactic=smt sat.euf=true delta.smt2
num-conflicts: 4
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 2537
Failed to verify: idx > 0

Z3 4.8.16.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
$ cat delta.smt2
(define-sort FP () (_ FloatingPoint 3 5))
(assert (distinct false (exists ((x FP)) (distinct x (fp.sub RTN x x)))))
(check-sat)

z3 4b14192

merlinsun · 2022-03-22T08:00:57Z

$ z3-debug tactic.default_tactic=smt sat.euf=true case.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_solver.cpp
Line: 226
s().value(lit) == l_true
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C
$ cat case.smt2
(declare-fun v () (Array Bool Bool))
(declare-fun va () (Array (Array Bool Bool) Bool))
(declare-fun a () (Array Bool Bool))
(assert (not (xor false false false false false false false false false false false (and false (= true (select (store (store va a (select v true)) v true) (store v false false)))))))
(check-sat)

regression when tracking literal explanations

merlinsun · 2022-03-24T03:14:30Z

A much simpler instance related to #5778 (comment):

# cat delta.smt2
(declare-const x Bool)
(set-option :rewriter.flat false)
(declare-fun e () (_ BitVec 64))
(assert (or (and x (fp.geq ((_ to_fp 11 53) e) ((_ to_fp 11 53) (_ bv0 64)))) (fp.geq ((_ to_fp 11 53) e) (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)))))
(check-sat-using sat-preprocess)
# z3debug delta.smt2 tactic.default_tactic=smt sat.euf=true
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C

merlinsun · 2022-03-27T03:56:20Z

An instance hard to reduce:

$ z3release tactic.default_tactic=smt sat.euf=true case.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_solver.cpp
Line: 618
Failed to verify: lit.var() == v

Z3 4.8.16.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
$ z3debug tactic.default_tactic=smt sat.euf=true case.smt2
ASSERTION VIOLATION
File: ../src/sat/tactic/goal2sat.cpp
Line: 263
!m_app2lit.contains(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C^C
$ cat case.smt2
(declare-sort L)
(declare-sort S)
(declare-sort F)
(declare-sort tra)
(declare-fun p (tra S L) L)
(declare-fun s (L) S)
(declare-fun u (S F tra L L Int) Bool)
(declare-fun r (F L) Int)
(declare-fun i (S S) S)
(declare-fun l (F tra L L Int) S)
(declare-fun r (tra L) L)
(declare-fun w (tra L L) tra)
(declare-fun i (L S) Bool)
(declare-fun B (tra L L L) Bool)
(declare-fun a () Bool)
(declare-fun t () L)
(declare-fun r14 () Bool)
(declare-fun ar1 () Bool)
(declare-fun xt () L)
(declare-fun tra () S)
(declare-fun a_ () Bool)
(declare-fun xtr () L)
(declare-fun x () L)
(declare-fun ar () Bool)
(declare-fun xtra () tra)
(declare-fun va () (_ BitVec 32))
(declare-fun r15 () Bool)
(declare-fun r6 () (_ BitVec 8))
(declare-fun r4 () (_ BitVec 32))
(declare-fun _v () Bool)
(declare-fun r19 () Bool)
(declare-fun r1 () Bool)
(declare-fun var () Bool)
(declare-fun ra () F)
(declare-fun tr () L)
(declare-fun v () Bool)
(assert (or (xor (B xtra xtr xtr t) (= tra (s xtr)) (i xtr (s xtr)) (= v r1) ar false (and (i xt tra) false (= xtr (r (w xtra xtr (r xtra xtr)) xtr)) (distinct (ite true false (ite r15 true a)) r15 r19 ar1) var (= r4 (bvand va (_ bv255 32)))) (B xtra xtr xtr xtr) (and ar (= (_ bv1 32) ((_ sign_extend 24) r6)))) (= xtr tr)))
(assert (or (or (i (p xtra (s xtr) (r xtra xtr)) (s xtr)) (= r14 false) (and (distinct (_ bv0 1) (bvcomp (_ bv0 1) (_ bv1 1))) (or true (= t xtr) (i xtr tra) (B xtra xtr xtr x) (= (s xtr) (i tra tra)) (u tra ra xtra xtr xtr (r ra xtr)) (i xt (l ra xtra xtr xtr (r ra xtr)))) (u tra ra xtra (r xtra xtr) (r xtra xtr) (r ra xtr)) a_ (B xtra x xtr (r xtra xtr)) _v (= (r xtra t) (r xtra t)) (or (= false false))) (= xtr (r xtra xtr)) ar)))
(assert (not (exists ((xt Bool) (E L)) xt)))
(check-sat)

merlinsun · 2022-03-27T15:22:42Z

memory leaks

# cat case.smt2
(declare-const x Int)
(declare-fun e () Int)
(assert (forall ((t Int) (ex Int)) (or (= 0 (* e t)) (= ex (+ (* x x) (* x ex x))))))
(check-sat)
# z3 case.smt2 tactic.default_tactic=smt sat.euf=true
sat

=================================================================
==35385==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 16 byte(s) in 1 object(s) allocated from:
    #0 0x7f1ae98ee808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x5620351fbf96 in memory::allocate(unsigned long) (/root/z3/build/z3+0x660df96)
    #2 0x5620320f57cb in q::interpreter::mk_depth1_vector(euf::enode*, func_decl*, unsigned int) (/root/z3/build/z3+0x35077cb)
    #3 0x5620320f7a99 in q::interpreter::init_continue(q::cont const*, unsigned int) (/root/z3/build/z3+0x3509a99)
    #4 0x5620321014a4 in q::interpreter::execute_core(q::code_tree*, euf::enode*) (/root/z3/build/z3+0x35134a4)
    #5 0x562032147661 in q::mam_impl::propagate() (/root/z3/build/z3+0x3559661)
    #6 0x562032054b3b in q::ematch::propagate(bool) (/root/z3/build/z3+0x3466b3b)
    #7 0x562031d2c85f in euf::solver::unit_propagate() (/root/z3/build/z3+0x313e85f)
    #8 0x56203433d2c8 in sat::solver::propagate_core(bool) (/root/z3/build/z3+0x574f2c8)
    #9 0x56203437cd8b in sat::solver::basic_search() (/root/z3/build/z3+0x578ed8b)
    #10 0x56203437db5a in sat::solver::bounded_search() (/root/z3/build/z3+0x578fb5a)
    #11 0x56203437eee5 in sat::solver::check(unsigned int, sat::literal const*) (/root/z3/build/z3+0x5790ee5)
    #12 0x562031ccd1a6 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30df1a6)
    #13 0x562031cd26f4 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e46f4)
    #14 0x56203307efe8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x4490fe8)
    #15 0x56203311ad99 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x452cd99)
    #16 0x56203311d7e6 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x452f7e6)
    #17 0x562032ee4cf9 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/root/z3/build/z3+0x42f6cf9)
    #18 0x562032ede49e in solver_na2as::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x42f049e)
    #19 0x562032f61034 in combined_solver::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x4373034)
    #20 0x562032f2fa27 in solver::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x4341a27)
    #21 0x562032e196f5 in cmd_context::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x422b6f5)
    #22 0x562032d78e78 in smt2::parser::operator()() (/root/z3/build/z3+0x418ae78)
    #23 0x562032d0a6d1 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x411c6d1)
    #24 0x56202f35978a in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76b78a)
    #25 0x56202f31269a in main (/root/z3/build/z3+0x72469a)
    #26 0x7f1ae92a40b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)

Indirect leak of 32 byte(s) in 1 object(s) allocated from:
    #0 0x7f1ae98ee808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x5620351fbf96 in memory::allocate(unsigned long) (/root/z3/build/z3+0x660df96)
    #2 0x56203211280e in vector<euf::enode*, false, unsigned int>::push_back(euf::enode* const&) (/root/z3/build/z3+0x352480e)
    #3 0x5620320f5abe in q::interpreter::mk_depth1_vector(euf::enode*, func_decl*, unsigned int) (/root/z3/build/z3+0x3507abe)
    #4 0x5620320f7a99 in q::interpreter::init_continue(q::cont const*, unsigned int) (/root/z3/build/z3+0x3509a99)
    #5 0x5620321014a4 in q::interpreter::execute_core(q::code_tree*, euf::enode*) (/root/z3/build/z3+0x35134a4)
    #6 0x562032147661 in q::mam_impl::propagate() (/root/z3/build/z3+0x3559661)
    #7 0x562032054b3b in q::ematch::propagate(bool) (/root/z3/build/z3+0x3466b3b)
    #8 0x562031d2c85f in euf::solver::unit_propagate() (/root/z3/build/z3+0x313e85f)
    #9 0x56203433d2c8 in sat::solver::propagate_core(bool) (/root/z3/build/z3+0x574f2c8)
    #10 0x56203437cd8b in sat::solver::basic_search() (/root/z3/build/z3+0x578ed8b)
    #11 0x56203437db5a in sat::solver::bounded_search() (/root/z3/build/z3+0x578fb5a)
    #12 0x56203437eee5 in sat::solver::check(unsigned int, sat::literal const*) (/root/z3/build/z3+0x5790ee5)
    #13 0x562031ccd1a6 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30df1a6)
    #14 0x562031cd26f4 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e46f4)
    #15 0x56203307efe8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x4490fe8)
    #16 0x56203311ad99 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x452cd99)
    #17 0x56203311d7e6 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x452f7e6)
    #18 0x562032ee4cf9 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/root/z3/build/z3+0x42f6cf9)
    #19 0x562032ede49e in solver_na2as::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x42f049e)
    #20 0x562032f61034 in combined_solver::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x4373034)
    #21 0x562032f2fa27 in solver::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x4341a27)
    #22 0x562032e196f5 in cmd_context::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x422b6f5)
    #23 0x562032d78e78 in smt2::parser::operator()() (/root/z3/build/z3+0x418ae78)
    #24 0x562032d0a6d1 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x411c6d1)
    #25 0x56202f35978a in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76b78a)
    #26 0x56202f31269a in main (/root/z3/build/z3+0x72469a)
    #27 0x7f1ae92a40b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)

SUMMARY: AddressSanitizer: 48 byte(s) leaked in 2 allocation(s).

zhendongsu · 2022-03-30T21:20:23Z

Invalid model:

[593] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[594] % cat small.smt2
(set-option :rewriter.expand_store_eq true)
(set-option :model_evaluator.array_equalities false)
(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(declare-fun c ((Array Int Int) (Array Int Int)) Int)
(assert (distinct 0 (select a (c b (store a 0 0)))))
(check-sat)

zhendongsu · 2022-03-31T14:56:15Z

[510] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[511] % cat small.smt2
(declare-fun x0 () (Array (_ BitVec 32) (_ BitVec 8)))

(assert (fp.isPositive ((_ to_fp 11 53) (concat (select x0 (_ bv31
  32)) (select x0 (_ bv0 32)) (select x0 (_ bv1 32)) (select x0 (_ bv0
  32)) (select x0 (_ bv27 32)) (select x0 (_ bv0 32)) (select x0 (_
  bv0 32)) (select x0 (_ bv1 32))))))

(assert (fp.lt ((_ to_fp 11 53) (concat (select x0 (_ bv31 32))
  (select x0 (_ bv30 32)) (select x0 (_ bv29 32)) (select x0 (_ bv28
  32)) (select x0 (_ bv27 32)) (select x0 (_ bv0 32)) (select x0 (_
  bv0 32)) (select x0 (_ bv24 32)))) ((_ to_fp 11 53) (concat (select
  x0 (_ bv0 32)) (select x0 (_ bv0 32)) (select x0 (_ bv13 32))
  (select x0 (_ bv0 32)) (select x0 (_ bv0 32)) (select x0 (_ bv10
  32)) (select x0 (_ bv0 32)) (select x0 (_ bv0 32))))))

(assert (or (fp.isNaN ((_ to_fp 11 53) (concat (select x0 (_ bv39 32))
  (select x0 (_ bv38 32)) (select x0 (_ bv37 32)) (select x0 (_ bv36
  32)) (select x0 (_ bv35 32)) (select x0 (_ bv34 32)) (select x0 (_
  bv33 32)) (select x0 (_ bv16 32))))) (fp.leq ((_ to_fp 11 53)
  (concat (select x0 (_ bv1 32)) (select x0 (_ bv0 32)) (select x0 (_
  bv37 32)) (select x0 (_ bv36 32)) (select x0 (_ bv35 32)) (select x0
  (_ bv34 32)) (select x0 (_ bv1 32)) (select x0 (_ bv16 32)))) ((_
  to_fp 11 53) (concat (select x0 (_ bv0 32)) (select x0 (_ bv30 32))
  (select x0 (_ bv29 32)) (select x0 (_ bv1 32)) (select x0 (_ bv27
  32)) (select x0 (_ bv0 32)) (select x0 (_ bv1 32)) (select x0 (_ bv0
  32)))))))

(assert (fp.geq ((_ to_fp 11 53) (concat (select x0 (_ bv39 32))
  (select x0 (_ bv38 32)) (select x0 (_ bv37 32)) (select x0 (_ bv36
  32)) (select x0 (_ bv35 32)) (select x0 (_ bv34 32)) (select x0 (_
  bv33 32)) (select x0 (_ bv16 32)))) ((_ to_fp 11 53) (concat (select
  x0 (_ bv15 32)) (select x0 (_ bv0 32)) (select x0 (_ bv13 32))
  (select x0 (_ bv0 32)) (select x0 (_ bv1 32)) (select x0 (_ bv10
  32)) (select x0 (_ bv1 32)) (select x0 (_ bv0 32))))))

(assert (fp.geq (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53)
  (concat (select x0 (_ bv39 32)) (select x0 (_ bv38 32)) (select x0
  (_ bv1 32)) (select x0 (_ bv0 32)) (select x0 (_ bv0 32)) (select x0
  (_ bv0 32)) (select x0 (_ bv0 32)) (select x0 (_ bv0 32))))))

(assert (fp.isPositive ((_ to_fp 11 53) (concat (select x0 (_ bv15
  32)) (select x0 (_ bv1 32)) (select x0 (_ bv2 32)) (select x0 (_ bv0
  32)) (select x0 (_ bv0 32)) (select x0 (_ bv0 32)) (select x0 (_ bv0
  32)) (select x0 (_ bv0 32))))))

(check-sat-using ufbv)

merlinsun · 2022-04-02T06:55:35Z

SEGV

$ cat delta.smt2
(declare-fun e () (Array Int (Array Int Real)))
(assert (forall ((x Int)) (= (> x 0) (= (select (select e 0) 1) (select (select e 0) x)))))
(check-sat-using default)
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==14367==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x556fd2f45daa bp 0x7fffbdb95c90 sp 0x7fffbdb95be0 T0)
==14367==The signal is caused by a READ memory access.
==14367==Hint: address points to the zero page.
    #0 0x556fd2f45da9 in ast_manager::is_value(expr*) const (/root/z3/build/z3+0x5bd1da9)
    #1 0x556fd19a8d7d in func_interp::insert_new_entry(expr* const*, expr*) (/root/z3/build/z3+0x4634d7d)
    #2 0x556fd078e9fa in array::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) (/root/z3/build/z3+0x341a9fa)
    #3 0x556fd0498de5 in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) (/root/z3/build/z3+0x3124de5)
    #4 0x556fd049d130 in euf::solver::update_model(ref<model>&) (/root/z3/build/z3+0x3129130)
    #5 0x556fcecbe215 in inc_sat_solver::get_model_core(ref<model>&) (/root/z3/build/z3+0x194a215)
    #6 0x556fd0785d72 in q::mbqi::check_forall(quantifier*) (/root/z3/build/z3+0x3411d72)
    #7 0x556fd07868c1 in q::mbqi::operator()() (/root/z3/build/z3+0x34128c1)
    #8 0x556fd04db808 in q::solver::check() (/root/z3/build/z3+0x3167808)
    #9 0x556fd04b53ee in euf::solver::check() (/root/z3/build/z3+0x31413ee)
    #10 0x556fd2b0c81d in sat::solver::basic_search() (/root/z3/build/z3+0x579881d)
    #11 0x556fd2b0cf8a in sat::solver::bounded_search() (/root/z3/build/z3+0x5798f8a)
    #12 0x556fd2b0e315 in sat::solver::check(unsigned int, sat::literal const*) (/root/z3/build/z3+0x579a315)
    #13 0x556fd04537d6 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30df7d6)
    #14 0x556fd0458d24 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e4d24)
    #15 0x556fd180e248 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449a248)
    #16 0x556fd181c6a2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x44a86a2)
    #17 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #18 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #19 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #20 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #21 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #22 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #23 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #24 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #25 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #26 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #27 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #28 0x556fd180fee8 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449bee8)
    #29 0x556fd181c6a2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x44a86a2)
    #30 0x556fd18a9ff9 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x4535ff9)
    #31 0x556fd18aca46 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x4538a46)
    #32 0x556fd153151a in check_sat_using_tactic_cmd::execute(cmd_context&) (/root/z3/build/z3+0x41bd51a)
    #33 0x556fd150235c in smt2::parser::parse_ext_cmd(int, int) (/root/z3/build/z3+0x418e35c)
    #34 0x556fd1507ddd in smt2::parser::operator()() (/root/z3/build/z3+0x4193ddd)
    #35 0x556fd1499931 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x4125931)
    #36 0x556fcdae00ea in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76c0ea)
    #37 0x556fcda98ffa in main (/root/z3/build/z3+0x724ffa)
    #38 0x7f75f035a0b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
    #39 0x556fcdab214d in _start (/root/z3/build/z3+0x73e14d)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/root/z3/build/z3+0x5bd1da9) in ast_manager::is_value(expr*) const
==14367==ABORTING

z3 4cc3327

merlinsun · 2022-04-02T07:09:56Z

SEGV

$ z3 tactic.default_tactic=smt sat.euf=true case.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==32516==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x5555b4efb696 bp 0x7ffc62878850 sp 0x7ffc62878770 T0)
==32516==The signal is caused by a READ memory access.
==32516==Hint: address points to the zero page.
    #0 0x5555b4efb695 in ast_manager::are_equal(expr*, expr*) const (/root/z3/build/z3+0x5bd2695)
    #1 0x5555b395e873 in func_interp::insert_entry(expr* const*, expr*) (/root/z3/build/z3+0x4635873)
    #2 0x5555b27439fa in array::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) (/root/z3/build/z3+0x341a9fa)
    #3 0x5555b244dde5 in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) (/root/z3/build/z3+0x3124de5)
    #4 0x5555b2452130 in euf::solver::update_model(ref<model>&) (/root/z3/build/z3+0x3129130)
    #5 0x5555b0c73215 in inc_sat_solver::get_model_core(ref<model>&) (/root/z3/build/z3+0x194a215)
    #6 0x5555b273ad72 in q::mbqi::check_forall(quantifier*) (/root/z3/build/z3+0x3411d72)
    #7 0x5555b273b8c1 in q::mbqi::operator()() (/root/z3/build/z3+0x34128c1)
    #8 0x5555b2490808 in q::solver::check() (/root/z3/build/z3+0x3167808)
    #9 0x5555b246a3ee in euf::solver::check() (/root/z3/build/z3+0x31413ee)
    #10 0x5555b4ac181d in sat::solver::basic_search() (/root/z3/build/z3+0x579881d)
    #11 0x5555b4ac1f8a in sat::solver::bounded_search() (/root/z3/build/z3+0x5798f8a)
    #12 0x5555b4ac3315 in sat::solver::check(unsigned int, sat::literal const*) (/root/z3/build/z3+0x579a315)
    #13 0x5555b24087d6 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30df7d6)
    #14 0x5555b240dd24 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e4d24)
    #15 0x5555b37c3248 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449a248)
    #16 0x5555b385eff9 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x4535ff9)
    #17 0x5555b3861a46 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x4538a46)
    #18 0x5555b3628f59 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/root/z3/build/z3+0x42fff59)
    #19 0x5555b36226fe in solver_na2as::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x42f96fe)
    #20 0x5555b36a5294 in combined_solver::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x437c294)
    #21 0x5555b3673c87 in solver::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x434ac87)
    #22 0x5555b355d955 in cmd_context::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x4234955)
    #23 0x5555b34bd0d8 in smt2::parser::operator()() (/root/z3/build/z3+0x41940d8)
    #24 0x5555b344e931 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x4125931)
    #25 0x5555afa950ea in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76c0ea)
    #26 0x5555afa4dffa in main (/root/z3/build/z3+0x724ffa)
    #27 0x7f0118b8c0b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
    #28 0x5555afa6714d in _start (/root/z3/build/z3+0x73e14d)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/root/z3/build/z3+0x5bd2695) in ast_manager::are_equal(expr*, expr*) const
==32516==ABORTING
$ cat case.smt2
(declare-const x Bool)
(declare-fun ar () (Array (_ BitVec 3) (Array (_ BitVec 2) Real)))
(declare-fun a () Real)
(assert (and (forall ((r Int)) (= (= 0 a) (= x (= r 0))))))
(assert (or (forall ((v Int)) true) (exists ((r (Array (_ BitVec 3) (Array (_ BitVec 2) Real)))) (distinct r ar))))
(check-sat)

add new clauses created during propagation to use-list

deal with recursive calls to internalization with the same formula

merlinsun · 2022-04-03T02:53:43Z

For this instance, I'm not sure if it deserves to be addressed since it contains strings to some extent.

$ cat delta.smt2
(declare-fun b (Int Int Int) Bool)
(declare-fun v () (Set String))
(declare-fun a () (Set String))
(assert (or (xor (subset a v) (b 0 0 0))))
(check-sat)
$ z3release tactic.default_tactic=smt sat.euf=true delta.smt2
unknown

=================================================================
==14626==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 192 byte(s) in 6 object(s) allocated from:
    #0 0x7f9b04776808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x557e77d196d6 in memory::allocate(unsigned long) (/root/z3/build/z3+0x66186d6)
    #2 0x557e74b18d6e in array::solver::get_select_set(euf::enode*) (/root/z3/build/z3+0x3417d6e)
    #3 0x557e74b2bf20 in array::solver::collect_selects() (/root/z3/build/z3+0x342af20)
    #4 0x557e74828656 in euf::solver::update_model(ref<model>&) (/root/z3/build/z3+0x3127656)
    #5 0x557e747e2d4d in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e1d4d)
    #6 0x557e747e59a4 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e49a4)
    #7 0x557e75b9baf8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449aaf8)
    #8 0x557e75c378b9 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x45368b9)
    #9 0x557e75c3a306 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x4539306)
    #10 0x557e75a01809 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/root/z3/build/z3+0x4300809)
    #11 0x557e759fafae in solver_na2as::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x42f9fae)
    #12 0x557e75a7db44 in combined_solver::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x437cb44)
    #13 0x557e75a4c537 in solver::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x434b537)
    #14 0x557e75936205 in cmd_context::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x4235205)
    #15 0x557e75895988 in smt2::parser::operator()() (/root/z3/build/z3+0x4194988)
    #16 0x557e758271e1 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x41261e1)
    #17 0x557e71e6d18a in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76c18a)
    #18 0x557e71e2609a in main (/root/z3/build/z3+0x72509a)
    #19 0x7f9b0412c0b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
......
SUMMARY: AddressSanitizer: 1176 byte(s) leaked in 14 allocation(s).
$ z3debug tactic.default_tactic=smt sat.euf=true delta.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/array_model.cpp
Line: 71
a.is_array(n->get_expr())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Try again when strings are supported

merlinsun · 2022-04-03T03:06:13Z

$ z3 tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (= (store r!0 false 1) (select a!1 0))
evaluated to false
(params drat.file null keep_cardinality_constraints true pb.solver solver)
false |-> 2
(= (store r!0 false 1) (select a!1 0)) |-> 3
$ cat small.smt2
(assert (forall ((r (Array Bool Int)) (a (Array Int (Array Bool Int)))) (distinct (store r false 1) (a 0))))
(check-sat)

zhendongsu · 2022-04-03T11:22:45Z

[543] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 667 5497: (= 8 (array-ext[0] d!2 (store #4938 2 #7542))) false
(sat
...
[544] % cat small.smt2
(declare-fun a ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((b Int) (c Int) (d (Array Int (Array Int Real)))) (or (= c 0) (= (select d 1) (select (a d) b)))))
(check-sat)

zhendongsu · 2022-04-03T11:24:34Z

[549] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 589 15070: (<= (+ (* 2 #2701) (* -1 #16145)) 0) false
(sat
...
[550] % cat small.smt2 
(declare-fun x () Int)
(declare-fun p (Int) Int)
(declare-fun x0 () Int)
(assert (> (p x0) 1))
(assert (and (forall ((i Int)) (=> (> i 0) (= (p i) (* 2 (p (- i 1))))))))
(check-sat)

merlinsun · 2022-04-05T02:43:09Z

SEGV

$ cat delta.smt2
(declare-fun r () (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool)))))))))
(declare-fun var () (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))
(declare-fun r7 () Int)
(declare-fun r76 () (Array (Array Int Bool) Bool))
(declare-fun v () (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))))
(declare-fun va () (Array Int Bool))
(declare-fun ar () Int)
(declare-fun a () (Array (Array Int Bool) Bool))
(assert (forall ((ar7 Int) (r9 Int) (r2 (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))) (xor (= r7 ar) (= r76 a) (= r9 0) (and (= var r2) (= r2 (store r2 v r))) (select va 1) (<= r9 0) (= r9 ar7))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==38763==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x56471766746a bp 0x7ffcdd5a3340 sp 0x7ffcdd5a3290 T0)
==38763==The signal is caused by a READ memory access.
==38763==Hint: address points to the zero page.
    #0 0x564717667469 in ast_manager::is_value(expr*) const (/root/z3/build/z3+0x5bd3469)
    #1 0x5647160ca1ed in func_interp::insert_new_entry(expr* const*, expr*) (/root/z3/build/z3+0x46361ed)
    #2 0x564714eaebfa in array::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) (/root/z3/build/z3+0x341abfa)
    #3 0x564714bb8cc5 in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) (/root/z3/build/z3+0x3124cc5)
    #4 0x564714bbd1d0 in euf::solver::update_model(ref<model>&) (/root/z3/build/z3+0x31291d0)
    #5 0x564714ea6fcf in q::mbqi::operator()() (/root/z3/build/z3+0x3412fcf)
    #6 0x564714bfb8a8 in q::solver::check() (/root/z3/build/z3+0x31678a8)
    #7 0x564714bd545e in euf::solver::check() (/root/z3/build/z3+0x314145e)
    #8 0x56471722dc8d in sat::solver::basic_search() (/root/z3/build/z3+0x5799c8d)
    #9 0x56471722e3fa in sat::solver::bounded_search() (/root/z3/build/z3+0x579a3fa)
    #10 0x56471722f785 in sat::solver::check(unsigned int, sat::literal const*) (/root/z3/build/z3+0x579b785)
    #11 0x564714b73466 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30df466)
    #12 0x564714b789b4 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x30e49b4)
    #13 0x564715f2f6a8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x449b6a8)
    #14 0x564715fcb469 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) (/root/z3/build/z3+0x4537469)
    #15 0x564715fcdeb6 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) (/root/z3/build/z3+0x4539eb6)
    #16 0x564715d953b9 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) (/root/z3/build/z3+0x43013b9)
    #17 0x564715d8eb5e in solver_na2as::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x42fab5e)
    #18 0x564715e116f4 in combined_solver::check_sat_core(unsigned int, expr* const*) (/root/z3/build/z3+0x437d6f4)
    #19 0x564715de00e7 in solver::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x434c0e7)
    #20 0x564715cc9db5 in cmd_context::check_sat(unsigned int, expr* const*) (/root/z3/build/z3+0x4235db5)
    #21 0x564715c29538 in smt2::parser::operator()() (/root/z3/build/z3+0x4195538)
    #22 0x564715bbad91 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/root/z3/build/z3+0x4126d91)
    #23 0x5647122001aa in read_smtlib2_commands(char const*) (/root/z3/build/z3+0x76c1aa)
    #24 0x5647121b90ba in main (/root/z3/build/z3+0x7250ba)
    #25 0x7f08e22a30b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
    #26 0x5647121d220d in _start (/root/z3/build/z3+0x73e20d)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/root/z3/build/z3+0x5bd3469) in ast_manager::is_value(expr*) const
==38763==ABORTING

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

merlinsun · 2022-04-07T08:08:54Z

$ cat delta.smt2
(declare-const _e (_ BitVec 16))
(declare-fun ex () (_ BitVec 32))
(declare-fun t () (_ BitVec 32))
(declare-fun e () Bool)
(assert (or (forall ((x Bool)) (exists ((e Bool)) (forall ((E Bool)) (or (forall ((e Bool)) e) (exists ((E Bool)) (or e (exists ((ex (_ BitVec 32))) (not (bvsle ((_ zero_extend 16) _e) ex))))))))) (forall ((E (_ BitVec 32))) (exists ((x (_ BitVec 32))) (and (exists ((V (_ BitVec 16))) (= ex (_ bv0 32))) (exists ((E Bool)) (or (bvsle x (_ bv0 32)) (exists ((E (_ BitVec 32))) (and (bvsle (bvadd t (bvmul ex (_ bv40 32))) (_ bv4820 32)) e)))))))))
(assert (forall ((x (_ BitVec 32)) (E (_ BitVec 32))) (bvsle (_ bv0 32) x)))
(check-sat)
$ z3debug tactic.default_tactic=smt sat.euf=true delta.smt2
Failed to validate ......


=================================================================
==46041==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 32 byte(s) in 4 object(s) allocated from:
    #0 0x7fec6a789808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x5581e1c0dfd1 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x5581e1c7ca6f in region::allocate(unsigned long) ../src/util/region.cpp:28
    #3 0x5581e0306650 in q::ematch::mk_justification(unsigned int, q::clause&, euf::enode* const*) ../src/sat/smt/q_ematch.cpp:127
    #4 0x5581e030a717 in q::ematch::propagate(bool, euf::enode* const*, unsigned int, q::clause&, bool&) ../src/sat/smt/q_ematch.cpp:365
    #5 0x5581e0309da5 in q::ematch::on_binding(quantifier*, app*, euf::enode* const*, unsigned int, unsigned int, unsigned int) ../src/sat/smt/q_ematch.cpp:331
    #6 0x5581e038dc51 in q::mam_impl::on_match(quantifier*, app*, unsigned int, euf::enode* const*, unsigned int) ../src/sat/smt/q_mam.cpp:3828
    #7 0x5581e035af68 in q::interpreter::execute_core(q::code_tree*, euf::enode*) ../src/sat/smt/q_mam.cpp:2511
    #8 0x5581e037cbf6 in q::interpreter::execute(q::code_tree*) ../src/sat/smt/q_mam.cpp:2036
    #9 0x5581e038cd68 in q::mam_impl::propagate_to_match() ../src/sat/smt/q_mam.cpp:3793
    #10 0x5581e038d0f4 in q::mam_impl::propagate() ../src/sat/smt/q_mam.cpp:3798
    #11 0x5581e030ebe3 in q::ematch::propagate(bool) ../src/sat/smt/q_ematch.cpp:615
    #12 0x5581e030ea5c in q::ematch::unit_propagate() ../src/sat/smt/q_ematch.cpp:611
    #13 0x5581e015dfc7 in q::solver::unit_propagate() ../src/sat/smt/q_solver.cpp:112
    #14 0x5581e0142344 in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:362
    #15 0x5581e1429b7f in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:1033
    #16 0x5581e1429dc4 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1045
    #17 0x5581e1435283 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1723
    #18 0x5581e14354b2 in sat::solver::search() ../src/sat/sat_solver.cpp:1736
    #19 0x5581e142f759 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1352
    #20 0x5581e010a38e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #21 0x5581e010cbae in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #22 0x5581e0b52e36 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1001
    #23 0x5581e0b85399 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #24 0x5581e0b85952 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:173
    #25 0x5581e0ab1415 in check_sat_core2 ../src/solver/tactic2solver.cpp:225
    #26 0x5581e0aae368 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #27 0x5581e0ad6053 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #28 0x5581e0aca138 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #29 0x5581e0a40d43 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
......
SUMMARY: AddressSanitizer: 56 byte(s) leaked in 7 allocation(s).

merlinsun · 2022-04-07T08:52:23Z

$ cat small.smt2
(declare-const x Bool)
(declare-const x4 Bool)
(declare-sort U)
(declare-fun m (U U) Bool)
(declare-fun v () (Array Int (Array Int Real)))
(declare-fun e () U)
(declare-fun a () (Array Int (Array Int Real)))
(assert (forall ((V Real)) (and (forall ((e U)) (exists ((v Real)) (and (m e e)))))))
(assert (exists ((v Real)) (and (forall ((V Real)) (= 1.0 (+ 1.0 (/ 0.6 v)))))))
(assert (or (and x4 x (m e e)) (distinct (and (= v a) (= v (store a 0 (select v 1)))))))
(check-sat)
$ z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 33 105: (= (select (select v #83) (array-ext[0] #85 #86)) (/ 3/5 v!0)) false
......

=================================================================
==26825==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 8 byte(s) in 1 object(s) allocated from:
    #0 0x7fc003727808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x55fcc1745fd1 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55fcc17b4a6f in region::allocate(unsigned long) ../src/util/region.cpp:28
    #3 0x55fcbfe3e650 in q::ematch::mk_justification(unsigned int, q::clause&, euf::enode* const*) ../src/sat/smt/q_ematch.cpp:127
    #4 0x55fcbfe42717 in q::ematch::propagate(bool, euf::enode* const*, unsigned int, q::clause&, bool&) ../src/sat/smt/q_ematch.cpp:365
    #5 0x55fcbfe41da5 in q::ematch::on_binding(quantifier*, app*, euf::enode* const*, unsigned int, unsigned int, unsigned int) ../src/sat/smt/q_ematch.cpp:331
    #6 0x55fcbfec5c51 in q::mam_impl::on_match(quantifier*, app*, unsigned int, euf::enode* const*, unsigned int) ../src/sat/smt/q_mam.cpp:3828
    #7 0x55fcbfe92f68 in q::interpreter::execute_core(q::code_tree*, euf::enode*) ../src/sat/smt/q_mam.cpp:2511
    #8 0x55fcbfec2f14 in q::mam_impl::propagate_new_patterns() ../src/sat/smt/q_mam.cpp:3723
    #9 0x55fcbfec5100 in q::mam_impl::propagate() ../src/sat/smt/q_mam.cpp:3799
    #10 0x55fcbfe46be3 in q::ematch::propagate(bool) ../src/sat/smt/q_ematch.cpp:615
    #11 0x55fcbfe46a5c in q::ematch::unit_propagate() ../src/sat/smt/q_ematch.cpp:611
    #12 0x55fcbfc95fc7 in q::solver::unit_propagate() ../src/sat/smt/q_solver.cpp:112
    #13 0x55fcbfc7a344 in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:362
    #14 0x55fcc0f61b7f in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:1033
    #15 0x55fcc0f61dc4 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1045
    #16 0x55fcc0f66e5a in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1314
    #17 0x55fcbfc4238e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #18 0x55fcbfc44bae in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #19 0x55fcc068ae36 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1001
    #20 0x55fcc06bd399 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #21 0x55fcc06bd952 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:173
    #22 0x55fcc05e9415 in check_sat_core2 ../src/solver/tactic2solver.cpp:225
    #23 0x55fcc05e6368 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #24 0x55fcc060e053 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #25 0x55fcc0602138 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #26 0x55fcc0578d43 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #27 0x55fcc052f994 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #28 0x55fcc0533e28 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #29 0x55fcc0535c7b in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162

SUMMARY: AddressSanitizer: 8 byte(s) leaked in 1 allocation(s).

reprogram flush, mark clauses during reinit as non-redundant.

…ted as shared Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

wintered · 2022-05-02T07:43:19Z

be653da

Possibly related to #6001 but no nonlinear mod and no variables in the assert.

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$cat bug.smt2 
(declare-const a Real) 
(assert (< (/ 0.0 0.0) 0.0)) 
(maximize a) 
(check-sat)
$

wintered · 2022-05-02T08:17:29Z

Another case without division by zero.

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
sat
(error "line 5 column 10: an invalid model was generated")
$cat bug.smt2 
(declare-const a Real) 
(declare-const b Real) 
(assert (> (to_int b) (+ 1 0))) 
(maximize a) 
(check-sat)
$

NikolajBjorner added a commit that referenced this issue Jan 17, 2022

#5778

a15da8f

NikolajBjorner added a commit that referenced this issue Jan 17, 2022

#5778

fcc9f37

NikolajBjorner added a commit that referenced this issue Jan 17, 2022

#5778

d777306

NikolajBjorner added a commit that referenced this issue Jan 21, 2022

#5778

9969809

NikolajBjorner added a commit that referenced this issue Jan 22, 2022

#5778

d02235f

not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.

NikolajBjorner added a commit that referenced this issue Jan 27, 2022

#5778

9e5b6e0

NikolajBjorner added a commit that referenced this issue Mar 21, 2022

#5778 - missed tracking literal assignment justification

20bd59b

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Mar 21, 2022

#5778

4b14192

NikolajBjorner added a commit that referenced this issue Mar 22, 2022

#5778

815c971

regression when tracking literal explanations

NikolajBjorner added a commit that referenced this issue Apr 1, 2022

#5778 #5937

81084b8

NikolajBjorner added a commit that referenced this issue Apr 1, 2022

#5778

c7922d6

NikolajBjorner added a commit that referenced this issue Apr 1, 2022

#5778

4cc3327

NikolajBjorner added a commit that referenced this issue Apr 2, 2022

#5778

97115e5

add new clauses created during propagation to use-list

NikolajBjorner added a commit that referenced this issue Apr 2, 2022

#5778

229ea56

NikolajBjorner added a commit that referenced this issue Apr 2, 2022

#5778

2fedcbd

NikolajBjorner added a commit that referenced this issue Apr 2, 2022

#5778

ef28f0e

deal with recursive calls to internalization with the same formula

NikolajBjorner added a commit that referenced this issue Apr 6, 2022

#5778 ensure else value so that defaults align across equivalence class

cebbc71

NikolajBjorner added a commit that referenced this issue Apr 6, 2022

#5778

2f63747

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Apr 9, 2022

#5778

f55b233

NikolajBjorner added a commit that referenced this issue Apr 25, 2022

#5778

489459a

reprogram flush, mark clauses during reinit as non-redundant.

NikolajBjorner added a commit that referenced this issue Apr 25, 2022

#5778

0a665b0

NikolajBjorner added a commit that referenced this issue Apr 25, 2022

#5778 - ensure arrays used inside of extensionality function are trea…

8e2f09b

…ted as shared Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner closed this as completed Apr 25, 2022

[consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778

[consolidated] issues for "tactic.default_tactic=smt sat.euf=true" #5778

Comments

rainoftime commented Jan 17, 2022 • edited Loading

rainoftime commented Jan 17, 2022 • edited Loading

rainoftime commented Jan 17, 2022 • edited Loading

rainoftime commented Jan 17, 2022

zhendongsu commented Jan 17, 2022

merlinsun commented Jan 19, 2022

zhendongsu commented Jan 19, 2022

merlinsun commented Jan 21, 2022 • edited Loading

zhendongsu commented Jan 21, 2022

zhendongsu commented Jan 21, 2022

zhendongsu commented Jan 21, 2022

zhendongsu commented Jan 21, 2022

zhendongsu commented Jan 22, 2022

zhendongsu commented Jan 23, 2022

zhendongsu commented Jan 26, 2022 • edited Loading

zhendongsu commented Jan 27, 2022

merlinsun commented Feb 5, 2022

merlinsun commented Feb 18, 2022 • edited by NikolajBjorner Loading

zhendongsu commented Mar 20, 2022

zhendongsu commented Mar 20, 2022

merlinsun commented Mar 22, 2022 • edited Loading

merlinsun commented Mar 22, 2022

merlinsun commented Mar 24, 2022 • edited Loading

merlinsun commented Mar 27, 2022

merlinsun commented Mar 27, 2022

zhendongsu commented Mar 30, 2022

zhendongsu commented Mar 31, 2022

merlinsun commented Apr 2, 2022

merlinsun commented Apr 2, 2022

merlinsun commented Apr 3, 2022 • edited by NikolajBjorner Loading

merlinsun commented Apr 3, 2022

zhendongsu commented Apr 3, 2022

zhendongsu commented Apr 3, 2022

merlinsun commented Apr 5, 2022

merlinsun commented Apr 7, 2022 • edited Loading

merlinsun commented Apr 7, 2022

wintered commented May 2, 2022 • edited Loading

wintered commented May 2, 2022 • edited Loading

rainoftime commented Jan 17, 2022 •

edited

Loading

rainoftime commented Jan 17, 2022 •

edited

Loading

rainoftime commented Jan 17, 2022 •

edited

Loading

merlinsun commented Jan 21, 2022 •

edited

Loading

zhendongsu commented Jan 26, 2022 •

edited

Loading

merlinsun commented Feb 18, 2022 •

edited by NikolajBjorner

Loading

merlinsun commented Mar 22, 2022 •

edited

Loading

merlinsun commented Mar 24, 2022 •

edited

Loading

merlinsun commented Apr 3, 2022 •

edited by NikolajBjorner

Loading

merlinsun commented Apr 7, 2022 •

edited

Loading

wintered commented May 2, 2022 •

edited

Loading

wintered commented May 2, 2022 •

edited

Loading