[consolidated] issues with new core #6523

NikolajBjorner · 2023-01-05T17:24:23Z

[554] % z3debug small.smt2
sat
[555] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 636
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[556] % cat small.smt2
(set-option :sat.prob_search true)
(define-sort a () (_ FloatingPoint 8 4))
(declare-fun b () a)
(assert (distinct (forall ((c a)) (distinct (fp.abs c) b))))
(check-sat-using (then purify-arith nra qe2))

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

NikolajBjorner · 2023-01-05T17:24:47Z

[529] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 76 147: (= (extract[31:31] (bv_wrap a)) (extract[31:31] (bv_wrap #80))) true
(sat
...
[530] % cat small.smt2
(declare-fun a () Float32)
(assert (forall ((b Float32)) (not (fp.isPositive (fp.max a b)))))
(check-sat)

zhendongsu · 2023-01-06T22:18:27Z

[568] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 162
(!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[569] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= a (* a (mod (to_int (/ 1 (* b b))) (to_int (/ (- 1 b) (- (abs 0))))))))
(check-sat)

merlinsun · 2023-02-13T07:07:36Z

$ z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/emonics.cpp
Line: 274
c == it->second
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2
(declare-const x Bool)
(declare-fun b (Real) Real)
(declare-fun v () Real)
(assert (or true (and x (< 1 0.0) (= 0 (b (/ 1 v v))))))
(check-sat)

zhendongsu · 2023-02-17T11:05:42Z

[518] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[519] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[520] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==27833==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000038 (pc 0x55ebe109da83 bp 0x7ffe1ef431d0 sp 0x7ffe1ef429a0 T0)
==27833==The signal is caused by a READ memory access.
==27833==Hint: address points to the zero page.
    #0 0x55ebe109da82 in euf::egraph::merge(euf::enode*, euf::enode*, euf::justification) ../src/ast/euf/euf_egraph.cpp:444
    #1 0x55ebddebae25 in euf::egraph::merge(euf::enode*, euf::enode*, void*) ../src/ast/euf/euf_egraph.h:254
    #2 0x55ebddebae25 in euf::solver::propagate_literal(euf::enode*, euf::enode*) ../src/sat/smt/euf_solver.cpp:482
    #3 0x55ebe1099e69 in std::function<void (euf::enode*, euf::enode*)>::operator()(euf::enode*, euf::enode*) const /usr/include/c++/7/bits/std_function.h:706
    #4 0x55ebe1099e69 in euf::egraph::add_literal(euf::enode*, euf::enode*) ../src/ast/euf/euf_egraph.cpp:161
    #5 0x55ebe1099e69 in euf::egraph::reinsert_equality(euf::enode*) ../src/ast/euf/euf_egraph.cpp:82
    #6 0x55ebe1099e69 in euf::egraph::reinsert_parents(euf::enode*, euf::enode*) ../src/ast/euf/euf_egraph.cpp:521
    #7 0x55ebe109f3c6 in euf::egraph::merge(euf::enode*, euf::enode*, euf::justification) ../src/ast/euf/euf_egraph.cpp:477
    #8 0x55ebddebdbfb in euf::egraph::merge(euf::enode*, euf::enode*, void*) ../src/ast/euf/euf_egraph.h:254
    #9 0x55ebddebdbfb in euf::solver::asserted(sat::literal) ../src/sat/smt/euf_solver.cpp:398
    #10 0x55ebe0e82018 in sat::solver::propagate_literal(sat::literal, bool) ../src/sat/sat_solver.cpp:1187
    #11 0x55ebe0e99159 in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:989
    #12 0x55ebe0eafd91 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1006
    #13 0x55ebe0eafd91 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1765
    #14 0x55ebe0eb08a1 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1758
    #15 0x55ebe0eb1939 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1308
    #16 0x55ebddea7831 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #17 0x55ebddeac03b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:221
    #18 0x55ebdfb0f29c in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032
    #19 0x55ebdfae4154 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #20 0x55ebdfae5b44 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:185
    #21 0x55ebdf906268 in check_sat_core2 ../src/solver/tactic2solver.cpp:236
    #22 0x55ebdf92ab1f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #23 0x55ebdf945534 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253
    #24 0x55ebdf9175a6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #25 0x55ebdf85a405 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1703
    #26 0x55ebdf7ac943 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #27 0x55ebdf7ac943 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #28 0x55ebdf7ac943 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
    #29 0x55ebdf761aa5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217
    #30 0x55ebdca1e641 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:182
    #31 0x55ebdc9e18f1 in main ../src/shell/main.cpp:389
    #32 0x7f7e00119c86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #33 0x55ebdc9f8879 in _start (/local/suz-local/software/z3san/build-02162023091711-bd10ddf/z3+0x232879)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_egraph.cpp:444 in euf::egraph::merge(euf::enode*, euf::enode*, euf::justification)
==27833==ABORTING
[521] % 
[521] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f (Bool) Int)
(declare-fun g () Int)
(declare-fun h () Int)
(assert (= (b h) (= (f (= e g)) a) (= c d)))
(assert (= c g))
(assert (= d e))
(check-sat)

merlinsun · 2023-03-06T09:52:54Z

42076a3

$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_etable.h
Line: 64
n1->get_decl() == n2->get_decl()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2
(set-option :tactic.default_tactic smt)
(set-option :sat.euf true)
(declare-fun a () (Array Bool Bool))
(declare-fun v () (Array (Array Bool Bool) Bool))
(declare-fun r () (Array Bool Bool))
(assert (forall ((va (Array Bool Bool))) (not (= (va (= va r)) (va (= va a))))))
(assert (select v r))
(check-sat)

merlinsun · 2023-03-06T12:21:22Z

$ cat small.smt2
(declare-fun b (Int Int Int Int Int Int) Bool)
(declare-fun r () (Array Bool Bool))
(declare-fun a () (Array Bool Int))
(declare-fun r11 () (Array Bool (Array Bool (Array Int Bool))))
(declare-fun va () (Array Int Int))
(declare-fun r111 () Bool)
(declare-fun ar () (Array Bool (Array Int Bool)))
(declare-fun var () Int)
(declare-fun r1 () (Array Int Int))
(declare-fun var1 () (Array Bool Int))
(declare-fun r5 () Int)
(declare-fun ar1 () Bool)
(declare-fun r10 () Int)
(declare-fun ar111 () Int)
(declare-fun v () Int)
(push)
(assert (and (forall ((V Int)) (> r5 var)) (forall ((v Int)) (exists ((v Int)) (not (not (distinct 10 v))))) (forall ((V Int)) (and (>= (- 8) r10) (= r10 (select a false)) (>= r10 (select a false)) (>= (- 0 r5 0 (select a false) (select a ar1)) 0))) (forall ((V Bool) (V Int) (var111 (Array Bool (Array Int Bool)))) (not (= r11 (store (store r11 false ar) (or (b 0 ar111 0 1 (select va v) (select var1 (select r (= r (store r r111 true))))) (not (b 0 0 0 (- 1) (select r1 0) (select var1 (select r ar1))))) var111))))))
(check-sat)
$ z3debug  tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault (core dumped)
$ z3asan tactic.default_tactic=smt sat.euf=true small.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==2074107==ERROR: AddressSanitizer: SEGV on unknown address 0x00207fff8007 (pc 0x55ac8f5fbe2d bp 0x7ffdeb831ea0 sp 0x7ffdeb831cd0 T0)
==2074107==The signal is caused by a READ memory access.
    #0 0x55ac8f5fbe2d in euf::etable::insert(euf::enode*) (/z3asan/build/z3+0x60ebe2d)
    #1 0x55ac8f5d8126 in euf::egraph::mk(expr*, unsigned int, unsigned int, euf::enode* const*) (/z3asan/build/z3+0x60c8126)
    #2 0x55ac8b606df6 in euf::solver::mk_enode(expr*, unsigned int, euf::enode* const*) (/z3asan/build/z3+0x20f6df6)
    #3 0x55ac8b639be1 in euf::th_euf_solver::mk_enode(expr*, bool) (/z3asan/build/z3+0x2129be1)
    #4 0x55ac8b7a0d16 in array::solver::post_visit(expr*, bool, bool) (/z3asan/build/z3+0x2290d16)
    #5 0x55ac8b6382fc in euf::th_internalizer::visit_rec(ast_manager&, expr*, bool, bool) (/z3asan/build/z3+0x21282fc)
    #6 0x55ac8b799bb4 in non-virtual thunk to array::solver::internalize(expr*, bool, bool) (/z3asan/build/z3+0x2289bb4)
    #7 0x55ac8b60b47c in euf::solver::internalize(expr*, bool, bool) (/z3asan/build/z3+0x20fb47c)
    #8 0x55ac8b543c39 in goal2sat::imp::convert_euf(expr*, bool, bool) (/z3asan/build/z3+0x2033c39)
    #9 0x55ac8b550118 in goal2sat::imp::convert_atom(expr*, bool, bool) (/z3asan/build/z3+0x2040118)
    #10 0x55ac8b55282b in goal2sat::imp::visit(expr*, bool, bool) (/z3asan/build/z3+0x204282b)
    #11 0x55ac8b555193 in goal2sat::imp::process(expr*, bool) (/z3asan/build/z3+0x2045193)
    #12 0x55ac8b55c5b9 in goal2sat::imp::internalize(expr*) (/z3asan/build/z3+0x204c5b9)
    #13 0x55ac8b6526d3 in euf::solver::finish_reinit() (/z3asan/build/z3+0x21426d3)
    #14 0x55ac8b65c346 in euf::solver::pop_reinit() (/z3asan/build/z3+0x214c346)
    #15 0x55ac8f26ecfc in sat::solver::pop(unsigned int) [clone .part.0] (/z3asan/build/z3+0x5d5ecfc)
    #16 0x55ac8f27017c in sat::solver::pop_reinit(unsigned int) (/z3asan/build/z3+0x5d6017c)
    #17 0x55ac8f28e7fc in sat::solver::check(unsigned int, sat::literal const*) (/z3asan/build/z3+0x5d7e7fc)
    #18 0x55ac8b0b3936 in inc_sat_solver::check_sat_core(unsigned int, expr* const*) (/z3asan/build/z3+0x1ba3936)
    #19 0x55ac8d7bc297 in combined_solver::check_sat_core(unsigned int, expr* const*) (/z3asan/build/z3+0x42ac297)
    #20 0x55ac8d796a47 in solver::check_sat(unsigned int, expr* const*) (/z3asan/build/z3+0x4286a47)
    #21 0x55ac8d6acd17 in cmd_context::check_sat(unsigned int, expr* const*) (/z3asan/build/z3+0x419cd17)
    #22 0x55ac8d6302e8 in smt2::parser::operator()() (/z3asan/build/z3+0x41202e8)
    #23 0x55ac8d5c81fd in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) (/z3asan/build/z3+0x40b81fd)
    #24 0x55ac89d04fe6 in read_smtlib2_commands(char const*) (/z3asan/build/z3+0x7f4fe6)
    #25 0x55ac89c8204b in main (/z3asan/build/z3+0x77204b)
    #26 0x7f6b2f40ed8f in __libc_start_call_main ../sysdeps/nptl/libc_start_call_main.h:58
    #27 0x7f6b2f40ee3f in __libc_start_main_impl ../csu/libc-start.c:392
    #28 0x55ac89c9f754 in _start (/z3asan/build/z3+0x78f754)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV (/z3asan/build/z3+0x60ebe2d) in euf::etable::insert(euf::enode*)
==2074107==ABORTING

merlinsun · 2023-03-06T14:12:50Z

$ z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 499
!m_table.contains_ptr(p)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2
(declare-const x Bool)
(declare-const x1 Bool)
(declare-fun a () Bool)
(declare-fun r7 () (Array Bool Real))
(declare-fun ar () (Array Bool (Array Bool Real)))
(declare-fun r1 () Bool)
(declare-fun va () Int)
(push)
(assert (not (exists ((r Bool) (v Int)) (xor a x1 (= v va) (= r7 (select ar r1)) (and x x1 (= 1 (select r7 r)))))))
(check-sat)

zhendongsu · 2023-03-26T20:36:31Z

[528] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/nla_core.cpp
Line: 169
(!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[529] % cat small.smt2
(set-option :smt.arith.ignore_int true)
(set-option :smt.random_seed 1)
(declare-fun a () Int)
(assert (= (* 2 a a) (+ a 1)))
(check-sat-using lia)

zhendongsu · 2023-03-27T07:25:44Z

[527] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 415
UNEXPECTED CODE WAS REACHED.
Z3 4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[528] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (or (= a 0) (= b 0)))
(check-sat-using (then add-bounds qfuf))

merlinsun · 2023-03-29T03:49:22Z

$ z3release tactic.default_tactic=smt sat.euf=true small.smt2  
-1 -1 -1 -1  >= 2
ASSERTION VIOLATION
File: ../src/sat/smt/pb_solver.cpp
Line: 1416
Failed to verify: c->well_formed()

Z3 4.12.2.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 small.smt2 
(assert ((_ at-most 2) false false false false))
(check-sat)

Edit: this isn't going to be a supported scenario.
Using sat.smt=true instead of sat.euf=true (and/or ditching tactic.default_tactic=smt) ensures proper pre-processing.

merlinsun · 2023-03-29T06:44:03Z

$ z3release tactic.default_tactic=smt sat.euf=true small.smt2 
unsat
$ z3-4.8.9 tactic.default_tactic=smt sat.euf=true small.smt2 
sat
$ cvc5 -q small.smt2
sat
$ cat small.smt2
(assert (= ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1))) ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1)))))
(check-sat)

zhendongsu · 2023-04-08T10:26:27Z

Refutation unsoundness:

[580] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[581] % cat small.smt2
(set-option :sat.prob_search true)
(set-option :rewriter.eq2ineq true)
(set-option :sat.cardinality.solver true)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (not (= a b)))
(assert (<= 0 a 4))
(assert (<= 0 b 5))
(check-sat-using (then purify-arith sat qfnia default))

merlinsun · 2023-04-10T01:00:56Z

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/tactic/goal2sat.cpp
Line: 272
!m_app2lit.contains(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(assert (> 0 ((_ at-most 1) false)))
(check-sat)

zhendongsu · 2023-04-10T12:42:28Z

[517] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
(select (t2 (di (- 30076) 11872) (di sb 26999) (- 1.0))
        ((_ array-ext 0)
          (t2 (di (- 20427) 26999) (di (- 82) 52587) qValp14!22)
          (t2 (di (- 30076) 11872) (di sb 26999) (- 1.0)))) := ((as const (Array Int Real)) 0.0)
(t1 (di qLp5!6 qUp6!7) qValp7!8) := ((as const (Array Int Real)) 43180.0)
(select (t2 (di (- 30076) 11872) (di sb 26999) (- 1.0))
        ((_ array-ext 0)
          (t2 (di (- 20427) 26999) (di (- 82) 52587) qValp14!22)
          (t2 (di (- 30076) 11872) (di sb 26999) (- 1.0)))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[518] % cat small.smt2
(set-option :smt.random_seed 13)
(set-option :rewriter.eq2ineq true)
(declare-fun x () Bool)
(declare-fun d () Real)
(declare-fun i () Real)
(declare-fun p () Int)
(declare-fun v () Real)
(declare-fun sb () Int)
(declare-fun s () Int)
(declare-fun sv () (Array Int Real))
(declare-fun sw () Int)
(declare-fun u () Real)
(declare-fun su (Int Int Real) Real)
(declare-fun di (Int Int) Int)
(declare-fun t1 (Int Real) (Array Int Real))
(declare-fun t2 (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((qI Int) (qLp5 Int) (qUp6 Int) (qValp7 Real)) (or
   (not (and (<= qLp5 qI) (< qI sw))) (= (select (t1
   (di qLp5 qUp6) qValp7) qI) qValp7))))
(assert (forall ((q Int) (qL Int) (qU1p10 Int) (qJp11 Int) (qL2p12
   Int) (qU2p13 Int) (qValp14 Real)) (=> (and (<= qL q) (<= 0 qU1p10)
   (<= qL2p12 qJp11) (<= qJp11 qU2p13)) (= (select (select
   (t2 (di qL qU1p10) (di qL2p12 qU2p13) qValp14) q)
   qJp11) qValp14))))
(assert (forall ((q Real)) (= 0.0 (su 0 (- 1) 1.0))))
(assert (distinct d u))
(assert (let ((qvp1 (= 0.0 v))) (not (=> and x (and (forall ((q Int))
   (or (< q 0) (= 0.0 (select sv 0)))) (and (and (forall ((q Int)) (=
   p i)) (or (forall ((q Int)) true) (and false (and (<= p 1) (and
   (and (< s 0) (<= sb 0)) (> sw 1)))))))) (= i v)))))
(check-sat)

merlinsun · 2023-04-12T09:40:06Z

$ cat delta.out.smt2 
(assert ((_ pbeq 1 0) ((_ pbeq 1 0) false)))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2 
ASSERTION VIOLATION
File: ../src/sat/tactic/goal2sat.cpp
Line: 783
i.m.limit().is_canceled() || is_root || rsz + 1 == r.size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-04-13T01:31:14Z

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 1966
m_mpz_manager.lt(o.significand, p_m3)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(declare-fun p () (_ FloatingPoint 2 3))
(declare-fun fp () (_ FloatingPoint 2 3))
(assert (fp.isNegative (fp.fma roundNearestTiesToEven fp p (fp (_ bv0 1) (_ bv0 2) (_ bv0 2)))))
(check-sat)

attach original variable to pb expression.

zhendongsu · 2023-08-16T19:48:52Z

[512] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[513] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[514] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==868321==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55c2959586a8 bp 0x7fff0cd07c90 sp 0x7fff0cd07a30 T0)
==868321==The signal is caused by a READ memory access.
==868321==Hint: address points to the zero page.
    #0 0x55c2959586a8 in ast::get_kind() const ../src/ast/ast.h:506
    #1 0x55c2959586a8 in is_app(ast const*) ../src/ast/ast.h:934
    #2 0x55c2959586a8 in is_ground(expr const*) ../src/ast/ast.h:1398
    #3 0x55c2959586a8 in var_subst::operator()(expr*, unsigned int, expr* const*) ../src/ast/rewriter/var_subst.cpp:30
    #4 0x55c2955be8c4 in mev::evaluator_cfg::evaluate_partial_theory_func(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:428
    #5 0x55c2955ca304 in mev::evaluator_cfg::reduce_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:293
    #6 0x55c2955d6f6c in mev::evaluator_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/model/model_evaluator.cpp:152
    #7 0x55c2955d6f6c in void rewriter_tpl<mev::evaluator_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:316
    #8 0x55c2955c699d in void rewriter_tpl<mev::evaluator_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:783
    #9 0x55c2955c699d in void rewriter_tpl<mev::evaluator_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:742
    #10 0x55c2955acf96 in rewriter_tpl<mev::evaluator_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/rewriter.h:360
    #11 0x55c2955acf96 in model_evaluator::operator()(expr*, obj_ref<expr, ast_manager>&) ../src/model/model_evaluator.cpp:758
    #12 0x55c2955acf96 in model_evaluator::operator()(expr*) ../src/model/model_evaluator.cpp:765
    #13 0x55c29551b0b4 in model::operator()(expr*) ../src/model/model.cpp:565
    #14 0x55c29551b0b4 in model::is_false(expr*) ../src/model/model.cpp:587
    #15 0x55c29377f7dc in euf::solver::validate_model(model&) ../src/sat/smt/euf_model.cpp:355
    #16 0x55c2937833b2 in euf::solver::update_model(ref<model>&, bool) ../src/sat/smt/euf_model.cpp:91
    #17 0x55c2935a235a in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:126
    #18 0x55c2935a3d74 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:221
    #19 0x55c2952a3c5e in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032
    #20 0x55c29528cda0 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #21 0x55c29528eafd 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:185
    #22 0x55c295061d0d in check_sat_core2 ../src/solver/tactic2solver.cpp:241
    #23 0x55c2950bf4c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #24 0x55c29507f644 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253
    #25 0x55c29507f644 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:211
    #26 0x55c2950591fc in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #27 0x55c294f7cdfc in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1776
    #28 0x55c294f22e93 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2632
    #29 0x55c294f22e93 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2972
    #30 0x55c294f22e93 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3190
    #31 0x55c294ecf30d in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3241
    #32 0x55c2921f0041 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:182
    #33 0x55c2921c4192 in main ../src/shell/main.cpp:384
    #34 0x7f8cbe93bd8f  (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f)
    #35 0x7f8cbe93be3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f)
    #36 0x55c2921e06f4 in _start (/local/home/suz/suz-local/software/z3san/build-08162023130730-1be6920/z3+0x76e6f4)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:506 in ast::get_kind() const
==868321==ABORTING
[515] % 
[515] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (> (div (to_int a) (to_int b)) (mod (to_int b) 2)))
(assert (= (- (* a (* a a))) (* 1 (* b b))))
(assert (not (= a 0)))
(check-sat)

zhendongsu · 2023-08-24T12:36:57Z

New core hangs on a very simple formula (appears to be a recent regression):

[517] % z3release small.smt2
sat
[518] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true small.smt2
Killed
[519] % cat small.smt2
(declare-fun a () Real)
(assert (or (< a 0) (or (<= 0 (+ (* 0) (* a 0))))))
(check-sat)

zhendongsu · 2023-09-02T20:13:55Z

[506] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
sat
sat
sat
sat
sat
sat
(f29 (f30 f31 23676) (v!1 (- 1))) := S14!val!12
(f29 (f30 f31 ?!65) v!64) := S14!val!1
(f29 (f30 f31 23676) (v!1 (- 1))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[507] % cat small.smt2
(declare-sort S 0)
(declare-sort S3 0)
(declare-sort S4 0)
(declare-sort S8 0)
(declare-sort S10 0)
(declare-sort S1 0)
(declare-sort S12 0)
(declare-sort S13 0)
(declare-sort S14 0)
(declare-sort S15 0)
(declare-sort S16 0)
(declare-sort S17 0)
(declare-sort S18 0)
(declare-fun f1 () S)
(declare-fun f (S3) S)
(declare-fun f7 () S4)
(declare-fun f () S8)
(declare-fun f22 (S10 Int) S)
(declare-fun f2 () S10)
(declare-fun f24 (S12 S1) Int)
(declare-fun f25 (S13 S1) S12)
(declare-fun f26 () S13)
(declare-fun f27 () S1)
(declare-fun f28 (S14 S15) S)
(declare-fun f29 (S16 S1) S14)
(declare-fun f30 (S17 Int) S16)
(declare-fun f31 () S17)
(declare-fun f3 (S18) S15)
(declare-fun f3 (S4) S18)
(push)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(assert (forall ((a Int)) (= (= f1 (f22 f2 a)) (forall ((v S1) (? Int)) (or (= a (- ? (f24 (f25 f26 v) f27))) (distinct f1 (f28 (f29 (f30 f31 ?) v) (f3 (f3 f7)))))))))
(check-sat)

merlinsun · 2023-09-22T01:43:25Z

fba5de3

$ cat small.smt2 
(set-option :tactic.default_tactic smt)
(set-option :sat.euf true)
(set-option :rewriter.eq2ineq true)
(declare-fun bug (Int Real) (Array Int Real))
(declare-fun a () Int)
(assert (forall ((var Real)) (= (select (bug 0 var) a) var)))
(check-sat)
$ z3 small.smt2 
(bug 0 (+ (- (/ 1.0 4.0)) (select (bug 0 var!0) a))) := (store ((as const (Array Int Real)) (- 56246.0)) 1323 (- (/ 7.0 4.0)))
(bug 0 var!20) := (store ((as const (Array Int Real)) 32392.0) 1323 (- 1.0))
(bug 0 (+ (- (/ 1.0 4.0)) (select (bug 0 var!0) a))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-09-25T07:44:53Z

$ cat small.smt2 
(declare-const x Bool)
(declare-fun b (Int Int) Bool)
(assert (forall ((v Int)) (or (= x (= v 0.0)) (= x (xor (b 0 0))))))
(check-sat-using sat)
$ z3asan tactic.default_tactic=smt sat.euf=true small.smt2 
unknown

=================================================================
==32749==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 56 byte(s) in 1 object(s) allocated from:
    #0 0x4bfbbd in malloc (/root/z3/build/z3+0x4bfbbd)
    #1 0x4a13281 in memory::allocate(unsigned long) /root/z3/build/../src/util/memory_manager.cpp:301:16
    #2 0x4a12ebf in memory::allocate(char const*, int, char const*, unsigned long) /root/z3/build/../src/util/memory_manager.cpp:228:16
    #3 0x19013df in q::ematch::clausify(quantifier*) /root/z3/build/../src/sat/smt/q_ematch.cpp:489:22
    #4 0x19036e4 in q::ematch::add(quantifier*) /root/z3/build/../src/sat/smt/q_ematch.cpp:579:21
    #5 0x160a48a in q::solver::asserted(sat::literal) /root/z3/build/../src/sat/smt/q_solver.cpp:71:26
    #6 0x15df0b3 in euf::solver::asserted(sat::literal) /root/z3/build/../src/sat/smt/euf_solver.cpp:407:39
    #7 0x3f13328 in sat::solver::propagate_literal(sat::literal, bool) /root/z3/build/../src/sat/sat_solver.cpp:1169:20
    #8 0x3f0f8d7 in sat::solver::propagate_core(bool) /root/z3/build/../src/sat/sat_solver.cpp:971:22
    #9 0x3f134b9 in sat::solver::propagate(bool) /root/z3/build/../src/sat/sat_solver.cpp:988:18
    #10 0x3f1795a in sat::solver::check(unsigned int, sat::literal const*) /root/z3/build/../src/sat/sat_solver.cpp:1261:13
    #11 0x1586c09 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/sat/tactic/sat_tactic.cpp:73:33
    #12 0x1584295 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/sat/tactic/sat_tactic.cpp:221:13
    #13 0x327c136 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:1032:14
    #14 0x327a8ae in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactical.cpp:874:14
    #15 0x32a9c9c in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /root/z3/build/../src/tactic/tactic.cpp:165:9
    #16 0x32aa514 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/../src/tactic/tactic.cpp:185:9
    #17 0x2ff483f in check_sat_using_tactic_cmd::execute(cmd_context&) /root/z3/build/../src/cmd_context/tactic_cmds.cpp:216:25
    #18 0x2fa163b in smt2::parser::parse_ext_cmd(int, int) /root/z3/build/../src/parsers/smt2/smt2parser.cpp:2930:33
    #19 0x2f98897 in smt2::parser::parse_cmd() /root/z3/build/../src/parsers/smt2/smt2parser.cpp:3040:13
    #20 0x2f9255f in smt2::parser::operator()() /root/z3/build/../src/parsers/smt2/smt2parser.cpp:3191:29
    #21 0x2f909ac in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /root/z3/build/../src/parsers/smt2/smt2parser.cpp:3242:12
    #22 0x508b13 in read_smtlib2_commands(char const*) /root/z3/build/../src/shell/smtlib_frontend.cpp:182:18
    #23 0x558ff7 in main /root/z3/build/../src/shell/main.cpp:384:28
    #24 0x7f53e9cbc082 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x24082)

Indirect leak of 88 byte(s) in 1 object(s) allocated from:
......

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

merlinsun · 2023-10-08T07:49:26Z

$ cat small.smt2 
(declare-fun b ((Array Int Int) Int) Int)
(declare-fun v () (Array Bool Bool))
(assert (forall ((va Int) (R Int) (r (Array Bool Bool)) (a (Array Int Int))) (or (not (= va (b a va))) (distinct true (r (= v r))))))
(check-sat)
$ z3asan tactic.default_tactic=smt sat.euf=true small.smt2 
=================================================================
==31706==ERROR: AddressSanitizer: heap-use-after-free on address 0x60f0000188a8 at pc 0x0000015af0d7 bp 0x7ffead5b73a0 sp 0x7ffead5b7398
READ of size 4 at 0x60f0000188a8 thread T0
    #0 0x15af0d6 in euf::enode::num_args() const /root/z3/build/../src/ast/euf/euf_enode.h:151:44
    #1 0x42237ce in euf::etable::cg_binary_eq::operator()(euf::enode*, euf::enode*) const /root/z3/build/../src/ast/euf/euf_etable.h:62:17
    #2 0x4221054 in chashtable<euf::enode*, euf::etable::cg_binary_hash, euf::etable::cg_binary_eq>::equals(euf::enode* const&, euf::enode* const&) const /root/z3/build/../src/util/chashtable.h:78:68
    #3 0x42149ba in chashtable<euf::enode*, euf::etable::cg_binary_hash, euf::etable::cg_binary_eq>::insert_if_not_there(euf::enode* const&) /root/z3/build/../src/util/chashtable.h:363:21
    #4 0x4210b5a in euf::etable::insert(euf::enode*) /root/z3/build/../src/ast/euf/euf_etable.cpp:212:48
    #5 0x41e55c0 in euf::egraph::insert_table(euf::enode*) /root/z3/build/../src/ast/euf/euf_egraph.cpp:72:27
   
......

SUMMARY: AddressSanitizer: heap-use-after-free /root/z3/build/../src/ast/euf/euf_enode.h:151:44 in euf::enode::num_args() const

zhendongsu · 2023-10-11T07:29:17Z

[515] % z3release tactic.default_tactic=smt sat.euf=true small.smt2 model_validate=true
sat
sat
failed to verify: (= h (b d l j j f (e d j)))
evaluated to false
(params keep_cardinality_constraints true pb.solver solver)
(<= i (e d j)) |-> 1
s!0 |-> 2
(= g (b d l j j f i)) |-> 3
(= h (b d l j j f (e d j))) |-> 4
(>= i (e d j)) |-> 5
(forall ((f a)) (= f j)) |-> 6
true |-> 7
[516] % cat small.smt2
(declare-sort a)
(declare-sort c)
(declare-sort k)
(declare-fun e (k a) Int)
(declare-fun b (k k a a Int Int) c)
(declare-fun d () k)
(declare-fun f () Int)
(declare-fun l () k)
(declare-fun g () c)
(declare-fun h () c)
(declare-fun i () Int)
(declare-fun j () a)
(assert (<= i (e d j)))
(check-sat (= g (b d l j j f i)))
(assert (= h (b d l j j f (e d j))))
(assert (>= i (e d j)))
(assert (forall ((f a)) (= f j)))
(check-sat)

zhendongsu · 2023-10-15T09:07:41Z

[549] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
sat
Failed to validate 3 12: (<= (c 0) (c a)) true
...
[550] % cat small.smt2 
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c (Int) Int)
(assert (= a b))
(push)
(check-sat)
(assert (< (c a) (c 0)))
(check-sat)

zhendongsu · 2023-10-15T09:16:58Z

[595] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
sat
sat
Failed to validate 21 81: (= (div (* -1 #46) (e 1)) (div0 (* -1 #46) (e 1))) false
...
[596] % cat small.smt2
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e (Int) Int)
(declare-fun f (Int) Int)
(define-fun k ((h Int)) Bool (and d (= h 0)))
(define-fun i ((a Int) (b Int)) Int (ite c a (mod a b)))
(define-fun l ((a Int)) Int (i (- (e 0) a) (e 0)))
(define-fun m ((b Int)) Int (i (- (e b)) (e 1)))
(define-fun n ((b Int)) Int (l b))
(assert c)
(push)
(push)
(push)
(declare-fun j () Int)
(check-sat)
(push)
(assert (k j))
(check-sat)
(assert (= (f (m (n 1))) 0))
(check-sat)

deal with memory leak when there is an exception

deal with memory leak on exceptions

fixup looping

merlinsun · 2023-10-16T09:26:13Z

cafe3ac

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_etable.cpp
Line: 241
!contains_ptr(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(declare-const x95 Bool)
(declare-const x8 Int)
(declare-const x91 Bool)
(declare-const x Bool)
(declare-const x9 Bool)
(declare-const x1 Int)
(declare-fun a () (Array Int (Array (Array Bool Bool) Bool)))
(declare-fun r () (Array Bool Bool))
(declare-fun r1 () (Array (Array Bool Bool) Bool))
(declare-fun r4 () (Array Bool Bool))
(declare-fun v () (Array Int (Array Int Bool)))
(assert (forall ((r Int)) (or (not (xor false (= r 0) (= 1 x8) x9)))))
(assert (and x91 x (select (select v 1) 1) (not (xor false false (or (= x1 0) (and x95 (distinct r1 (select a 0)))))) (select r4 (= r4 r))))
(check-sat)

zhendongsu · 2023-10-16T14:11:19Z

Hang on a small QF_NRA instance (it seems to be a recent regression):

[572] % timeout -s 9 30 z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Killed
[573] % cat small.smt2
(declare-fun a () Real)
(assert (< a 0))
(assert (= (* a a) 2))
(check-sat)

merlinsun · 2023-10-31T14:47:18Z

91c2139
Invalid model issue

$ cat small.smt2 
(declare-const x Bool)
(declare-fun v () Real)
(assert (> 1.0 (/ 1 v)))
(assert (and (forall ((a Real)) (or x (= 0 a)))))
(assert (= 0.0 (* (- 1.0) (- 1.0 v))))
(check-sat)
$ z3 model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")

merlinsun · 2023-11-01T02:52:17Z

$ cat small.smt2 
(set-option :tactic.default_tactic smt)
(set-option :sat.euf true)
(set-option :rewriter.eq2ineq true)
(declare-fun b (Int Int Real) (Array Int (Array Int Real)))
(declare-fun b (Int Int) Int)
(declare-fun v () (Array Bool (Array Bool Real)))
(declare-fun a () (Array Bool Real))
(assert (or (exists ((va Real)) (= a (select (store v (= va 1) a) false)))))
(assert (forall ((va Real)) (= (select (select (b 0 (b 0 0) va) 0) 0) va)))
(check-sat-using (then purify-arith default))

$ z3 small.smt2 
(let ((a!1 (select (select (b 0 (b 0 0) (- 1.0)) 0) 0)))
  (b 0 (b 0 0) (+ (- (/ 1.0 2.0)) a!1))) := (store ((as const (Array Int (Array Int Real)))
         ((as const (Array Int Real)) 1142.0))
       0
       ((as const (Array Int Real)) (- (/ 3.0 2.0))))
(b 0 (b 0 0) va!4) := ((as const (Array Int (Array Int Real))) ((as const (Array Int Real)) 1.0))
(let ((a!1 (select (select (b 0 (b 0 0) (- 1.0)) 0) 0)))
  (b 0 (b 0 0) (+ (- (/ 1.0 2.0)) a!1))) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-11-03T12:35:54Z

$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1931
validate_bound(j, kind, right_side, dep)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2 
(declare-fun v () Int)
(assert (forall ((r Bool)) (and (distinct v 0) (distinct 0 (div v (rem 0 0))))))
(check-sat)

zhendongsu · 2023-11-06T10:27:14Z

[512] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
=================================================================
==1251621==ERROR: AddressSanitizer: heap-use-after-free on address 0x60b000003850 at pc 0x55e99a94174b bp 0x7fffe619a760 sp 0x7fffe619a750
READ of size 8 at 0x60b000003850 thread T0
    #0 0x55e99a94174a in algebraic_numbers::anum::is_basic() const ../src/math/polynomial/algebraic_numbers.h:371
    #1 0x55e99a94174a in algebraic_numbers::manager::imp::compare(algebraic_numbers::anum&, algebraic_numbers::anum&) ../src/math/polynomial/algebraic_numbers.cpp:1951
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/math/polynomial/algebraic_numbers.h:371 in algebraic_numbers::anum::is_basic() const
...
[513] % 
[513] % cat small.smt2
(declare-fun l5 () Int)
(declare-fun l () Int)
(declare-fun a () Int)
(declare-fun m () Int)
(declare-fun la () Int)
(declare-fun am () Int)
(push)
(assert (or (and (= a 0) (= m 0) (> 0 (+ m (* l la)))) (and (>= la 0) (= am 0) (distinct (+ 1 l5) 0))))
(check-sat)

merlinsun · 2023-11-08T14:14:36Z

$ cat small.smt2 
(declare-const x Bool)
(declare-const x8 Bool)
(declare-fun a () Int)
(assert (= (= x (and x8 false)) (or (= (_ bv0 14) ((_ int2bv 14) a)))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 482
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-11-09T07:05:23Z

$ cat small.smt2 
(declare-const x Int)
(assert (forall ((v Int)) (and (= 0 (sin 1.0)) (= x (mod (- v) 33)))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 631
"integer variables should have integer values: " && (ctx.get_config().m_arith_ignore_int || !a.is_int(o) || r.is_int() || m.limit().is_canceled())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

zhendongsu · 2023-11-13T19:31:51Z

[514] % z3debug small.smt2
sat
sat
[515] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
sat
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 482
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[516] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(check-sat)
(assert (= a (- d)))
(assert (> c 0))
(assert (< 0 (+ (* d b) f)))
(assert (distinct 1 (- c d d)))
(assert (= 0 (+ 1 f e)))
(assert (= 0 (+ a a e 3)))
(check-sat)

zhendongsu · 2023-11-13T19:34:42Z

[527] % z3san tactic.default_tactic=smt sat.euf=true small.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==1157897==ERROR: AddressSanitizer: SEGV on unknown address 0x61e800051c80 (pc 0x55d3b5100b99 bp 0x7ffc881642b0 sp 0x7ffc88164040 T0)
==1157897==The signal is caused by a READ memory access.
    #0 0x55d3b5100b99 in euf::th_euf_solver::var2enode(int) const ../src/sat/smt/sat_th.h:212
    #1 0x55d3b5100b99 in arith::solver::is_equal(int, int) const ../src/sat/smt/arith_solver.cpp:748
    #2 0x55d3b5100b99 in arith::solver::is_equal(int, int) const ../src/sat/smt/arith_solver.cpp:747
    #3 0x55d3b5100b99 in arith::solver::add_eq(unsigned int, unsigned int, lp::explanation const&, bool) ../src/sat/smt/arith_solver.cpp:326
...
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/sat/smt/sat_th.h:212 in euf::th_euf_solver::var2enode(int) const
==1157897==ABORTING
[528] % 
[528] % cat small.smt2 
(declare-fun p (Int) Int)
(declare-fun i (Int Int Int) Int)
(declare-fun k () Int)
(assert (> k 0))
(assert (= 1 (p 0)))
(assert (forall ((i Int)) (= (p i) (p (- i 1)))))
(assert (forall ((a Int) (b Int)) (= (i 0 0 b) (* (mod a 2) (p (- k 1))))))
(check-sat)

regressions from changes inside math/lp/int_solver

malformed models on giveup status

merlinsun · 2023-11-14T11:18:26Z

$ cat small.smt2 
(declare-const x1 Bool)
(declare-const x Int)
(declare-const x2 Int)
(declare-const x13 Int)
(assert (and (>= (/ 1 x) 1)))
(assert (forall ((a Int)) (distinct (exists ((V Int)) x1) (<= x (+ 1 x2 x13 (* 16 a))))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1161
!column_is_int(j) || v.is_int()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-11-14T11:33:19Z

$ cat small.smt2 
(declare-fun b (Real Real) Real)
(declare-fun u (Real Real) (Array Real Real))
(assert (forall ((v Real) (r Real)) (= v (select (u v (b 0.0 0.0)) r))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true rewriter.eq2ineq=true small.smt2
(u (b 0.0 0.0) (b 0.0 0.0)) := ((as const (Array Real Real)) 0.0)
(u v!2 (b 0.0 0.0)) := ((as const (Array Real Real)) (- 1.0))
(u (b 0.0 0.0) (b 0.0 0.0)) -> ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 168
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

merlinsun · 2023-11-16T01:58:51Z

$ cat small.smt2 
(declare-fun b (Int Int Int Int Int Int) Bool)
(declare-fun v () (Array Bool Bool))
(declare-fun a () (Array Bool Int))
(declare-fun va () Bool)
(assert (forall ((r (Array Bool (Array Int Bool))) (ar (Array Bool (Array Bool (Array Int Bool))))) (distinct ar (store ar (or (b 1 0 0 1 0 (select a (select v (= v (store v va true)))))) r))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2 
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 565
!p->cgc_enabled() || m_table.contains_ptr(p)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

zhendongsu · 2023-11-20T19:43:21Z

[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
Failed to validate 60 741: (= (o (a #186)) (o (a #668))) false
(sat
...
[512] % cat small.smt2 
(declare-datatypes ((a 0)) (((a (o (Array (_ BitVec 2) (_ BitVec 2)))))))
(declare-fun r ((_ BitVec 2) a (_ BitVec 2)) Bool)
(assert (forall ((a a) (s (_ BitVec 2))) (= (bvsge s (_ bv0 2)) (r s a (_ bv0 2)))))
(check-sat)

merlinsun · 2023-11-26T11:09:28Z

$ cat small.smt2 
(declare-const x (Array (Array Bool Bool) Bool))
(declare-fun a () (Array (Array Bool Bool) Bool))
(declare-fun v () (Array Bool Bool))
(declare-fun r () (Array (Array Bool Bool) Bool))
(declare-fun r1 () (Array Int (Array (Array Bool Bool) Bool)))
(assert (forall ((V Int)) (distinct a r x (select r1 0))))
(assert (forall ((va (Array Bool Bool))) (va (= va v))))
(check-sat)
$ z3 small.smt2 tactic.default_tactic=smt sat.euf=true 
=================================================================
==26023==ERROR: AddressSanitizer: heap-use-after-free on address 0x60f00000b888 at pc 0x0000015b5e87 bp 0x7ffe38ef99e0 sp 0x7ffe38ef99d8
READ of size 4 at 0x60f00000b888 thread T0
    #0 0x15b5e86 in euf::enode::num_args() const /root/z3/build/../src/ast/euf/euf_enode.h:152:44
    #1 0x425bf8e in euf::etable::cg_binary_eq::operator()(euf::enode*, euf::enode*) const /root/z3/build/../src/ast/euf/euf_etable.h:62:17
    #2 0x4259814 in chashtable<euf::enode*, euf::etable::cg_binary_hash, euf::etable::cg_binary_eq>::equals(euf::enode* const&, euf::enode* const&) const /root/z3/build/../src/util/chashtable.h:78:68
    #3 0x424d17a in chashtable<euf::enode*, euf::etable::cg_binary_hash, euf::etable::cg_binary_eq>::insert_if_not_there(euf::enode* const&) /root/z3/build/../src/util/chashtable.h:363:21
    #4 0x424931a in euf::etable::insert(euf::enode*) /root/z3/build/../src/ast/euf/euf_etable.cpp:212:48
    #5 0x421dd40 in euf::egraph::insert_table(euf::enode*) /root/z3/build/../src/ast/euf/euf_egraph.cpp:74:27
    #6 0x422c67b in euf::egraph::reinsert_parents(euf::enode*, euf::enode*) /root/z3/build/../src/ast/euf/euf_egraph.cpp:521:40
...

SUMMARY: AddressSanitizer: heap-use-after-free /root/z3/build/../src/ast/euf/euf_enode.h:152:44 in euf::enode::num_args() const
...

merlinsun · 2023-11-29T02:17:20Z

$ cat small.smt2 
(assert (and (forall ((V Int)) (xor (exists ((v Int)) (< v 0))))))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 1534
f->get_family_id() == get_id()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

NikolajBjorner · 2023-11-30T16:32:36Z

Move to #7026 and #7027

NikolajBjorner mentioned this issue Jan 5, 2023

[consolidated] issues with new core #6429

Closed

NikolajBjorner added a commit that referenced this issue Jul 14, 2023

#6523

3849f66

NikolajBjorner added a commit that referenced this issue Aug 1, 2023

#6523

5b2519d

attach original variable to pb expression.

NikolajBjorner added a commit that referenced this issue Oct 15, 2023

#6523

5942dc2

NikolajBjorner added a commit that referenced this issue Oct 15, 2023

#6523

41b1f47

deal with memory leak when there is an exception

NikolajBjorner added a commit that referenced this issue Oct 15, 2023

#6523

b2efa59

deal with memory leak on exceptions

NikolajBjorner added a commit that referenced this issue Oct 15, 2023

#6523

891ab8b

fixup looping

NikolajBjorner added a commit that referenced this issue Oct 16, 2023

#6523

c9c5dbc

NikolajBjorner added a commit that referenced this issue Nov 7, 2023

#6523 and other heap-use-after-free error

e86eae2

NikolajBjorner added a commit that referenced this issue Nov 13, 2023

#6523

8a4e857

regressions from changes inside math/lp/int_solver

NikolajBjorner added a commit that referenced this issue Nov 13, 2023

#6523

c2610cb

malformed models on giveup status

NikolajBjorner added a commit that referenced this issue Nov 29, 2023

#6523 - contains_ptr bug regarding etable reinserts

e972eb3

NikolajBjorner closed this as completed Nov 30, 2023

[consolidated] issues with new core #6523

[consolidated] issues with new core #6523

Comments

NikolajBjorner commented Jan 5, 2023

NikolajBjorner commented Jan 5, 2023

zhendongsu commented Jan 6, 2023

merlinsun commented Feb 13, 2023

zhendongsu commented Feb 17, 2023

merlinsun commented Mar 6, 2023

merlinsun commented Mar 6, 2023

merlinsun commented Mar 6, 2023

zhendongsu commented Mar 26, 2023

zhendongsu commented Mar 27, 2023

merlinsun commented Mar 29, 2023 • edited by NikolajBjorner Loading

merlinsun commented Mar 29, 2023

zhendongsu commented Apr 8, 2023

merlinsun commented Apr 10, 2023

zhendongsu commented Apr 10, 2023

merlinsun commented Apr 12, 2023

merlinsun commented Apr 13, 2023

zhendongsu commented Aug 16, 2023

zhendongsu commented Aug 24, 2023

zhendongsu commented Sep 2, 2023

merlinsun commented Sep 22, 2023

merlinsun commented Sep 25, 2023

merlinsun commented Oct 8, 2023

zhendongsu commented Oct 11, 2023

zhendongsu commented Oct 15, 2023

zhendongsu commented Oct 15, 2023

merlinsun commented Oct 16, 2023

zhendongsu commented Oct 16, 2023

merlinsun commented Oct 31, 2023

merlinsun commented Nov 1, 2023

merlinsun commented Nov 3, 2023

zhendongsu commented Nov 6, 2023 • edited Loading

merlinsun commented Nov 8, 2023

merlinsun commented Nov 9, 2023

zhendongsu commented Nov 13, 2023

zhendongsu commented Nov 13, 2023

merlinsun commented Nov 14, 2023

merlinsun commented Nov 14, 2023

merlinsun commented Nov 16, 2023

zhendongsu commented Nov 20, 2023

merlinsun commented Nov 26, 2023

merlinsun commented Nov 29, 2023

NikolajBjorner commented Nov 30, 2023

merlinsun commented Mar 29, 2023 •

edited by NikolajBjorner

Loading

zhendongsu commented Nov 6, 2023 •

edited

Loading