8000 [Consolidated] issues affecting tactic.default_tactic=smt sat.euf=true · Issue #5532 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
rainoftime opened this issue Sep 3, 2021 · 37 comments
Closed

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

rainoftime opened this issue Sep 3, 2021 · 37 comments

Comments

@rainoftime
Copy link
Contributor
rainoftime commented Sep 3, 2021 •
edited
Loading

Hi, for the following formula,
z3 af5c6e4

(declare-sort A)
(declare-fun f (A) A)
(assert (forall ((x A)) (forall ((y A)) (and (= x (f (f x))) (= x y)))))
(check-sat)

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

src/sat/smt/bv_internalize.cpp:249

(declare-datatypes ((a 0)) (((e) (h (i (_ BitVec 1))))))
(declare-fun j (a) Bool)
(assert (forall ((m a)) (or (j m) (not ((_ is h) m)))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/bv_internalize.cpp
Line: 249
m_bits[v].back() == lit
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

@rainoftime
Copy link
Contributor Author

"Failed to validate" and leak

(set-option :sat.branching.heuristic chb)
(declare-fun f ((_ BitVec 3)) Int)
(declare-fun y () (_ BitVec 3))
(declare-fun A () (Array Int Int))
(assert (forall ((x (_ BitVec 3))) (not (= (select A (f (bvshl x y))) (select A (f (bvsdiv x (_ bv0 3))))))))
(check-sat)

@rainoftime
Copy link
Contributor Author
rainoftime commented Sep 3, 2021 •
edited
Loading

heap-use-after-free at ../src/sat/smt/q_mam.cpp:2939

(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth))))
(declare-fun S$cardinality (S$t$type) Int)
(declare-fun count$1 () (Array resource$type Int))
(declare-fun valid$1 () (Array resource$type BOOL))
(assert (forall ((handles (Array resource$type S$t$type))) (exists ((handles$1 (Array resource$type S$t$type))) (forall ((count (Array resource$type Int))) (forall ((valid (Array resource$type BOOL))) (let (($x308 (not (or (not (forall ((r resource$type)) (or (= Truth (valid r)) (= (count r) (S$cardinality (handles r)))))) (forall ((r resource$type)) (or (not (= Truth (select valid$1 r))) (= (select count$1 r) (S$cardinality (handles$1 r)))))))))))))))
(check-sat)

@rainoftime
Copy link
Contributor Author
rainoftime commented Sep 3, 2021 •
edited
Loading

src/sat/smt/arith_solver.cpp:594

(declare-fun arr () (Array Bool Int))
(declare-fun i10 () Int)
(assert (forall ((v18 Bool)) (forall ((i4 Int)) (and (not (= i10 0)) (<= (select (store arr v18 1) false) i4)))))
(check-sat)

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

@rainoftime
Copy link
Contributor Author

src/sat/sat_gc.cpp:461

(set-option :smt.ematching false)
(set-option :sat.branching.anti_exploration true)
(set-option :sat.branching.heuristic chb)
(declare-datatypes ((ColorType 0)) (((ColorType_Red) (ColorType_Black))))
(declare-datatypes ((RBTree_Node_recd 0) (RBTree 0)) (((RBTree_Node_recd (RBTree_Node_recd_color ColorType) (RBTree_Node_recd_left RBTree) (RBTree_Node_recd_elem Int) (RBTree_Node_recd_right RBTree))) ((RBTree_Leaf) (RBTree_Node (destRBTree_Node RBTree_Node_recd)))))
(declare-datatypes ((BoolColor 0)) (((BoolColor (BoolColor_res Bool) (BoolColor_color ColorType)))))
(declare-fun insertFn (Int RBTree) RBTree)
(declare-fun t () RBTree)
(declare-fun NoTwoRedsFn (RBTree) BoolColor)
(declare-fun insFn (Int RBTree) RBTree)
(assert (forall ((v0 Int)) (and (or ((_ is RBTree_Leaf) t) (and (not ((_ is RBTree_Leaf) (insertFn v0 t))) (not (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t)))))))) (= (insertFn v0 t) (insFn v0 t)) (= (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t)))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t)))) (BoolColor true ColorType_Black) (BoolColor (or (not (= ColorType_Red (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t))))))) (and (not (= (BoolColor_color (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node t)))))) ColorType_Red)) (not (= ColorType_Red (BoolColor_color (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t))))))))))) (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t)))))))) true (= (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node t))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node t))) (BoolColor true ColorType_Black) (BoolColor (and (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node t)))))) (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node t))))))) (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node t))))))) (= (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node t))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node t))) (BoolColor true ColorType_Black) (BoolColor (and (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node t)))))) (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node t)))))) (or (not (= ColorType_Red (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node t)))))) (= (BoolColor_color (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node t)))))) ColorType_Red))) (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node t))))))) (= (RBTree_Node_recd_left (destRBTree_Node t)) (insertFn v0 (RBTree_Node_recd_left (destRBTree_Node t)))) (= (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node t))) (BoolColor (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node t)))))) (RBTree_Node_recd_color (destRBTree_Node (insertFn v0 (RBTree_Node_recd_left (destRBTree_Node t))))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/sat_gc.cpp
Line: 461
!c->on_reinit_stack()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

@rainoftime
Copy link
Contributor Author
rainoftime commented Sep 3, 2021 •
edited
Loading

../src/sat/sat_gc.cpp:479

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

(set-option :sat.branching.anti_exploration true)
(set-option :sat.branching.heuristic chb)
(set-option :rewriter.elim_and true)
(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
(declare-sort data$type)
(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))))
(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort node$type)
(declare-fun auxnode () node$type)
(declare-fun shrset () (Array node$type BOOL))
(declare-fun exgntd () BOOL)
(declare-fun send_req_exclusive$i () node$type)
(declare-fun chan1 () (Array node$type msg$type))
(declare-fun chan1$1 () (Array node$type msg$type))
(declare-fun cache () (Array node$type cache$type))
(declare-fun l0 () Bool)
(declare-fun l1 () Bool)
(declare-fun l2 () Bool)
(declare-fun z3name!0 (node$type) BOOL)
(declare-fun l3 () Bool)
(declare-fun l4 () Bool)
(declare-fun n!3 () node$type)
(declare-fun l5 () Bool)
(declare-fun l6 () Bool)
(declare-fun l7 () Bool)
(declare-fun n!1 () node$type)
(declare-fun l8 () Bool)
(declare-fun l9 () Bool)
(declare-fun l11 () Bool)
(declare-fun l13 () Bool)
(declare-fun z3name!2 () BOOL)
(declare-fun l14 () Bool)
(declare-fun l15 () Bool)
(declare-fun l16 () Bool)
(declare-fun l17 () Bool)
(declare-fun l18 () Bool)
(declare-fun true () Bool)
(declare-fun l20 () Bool)
(declare-fun l21 () Bool)
(assert (= l13 (or (not (distinct chan1$1 (store chan1 send_req_exclusive$i (c_msg$type reqe (m_data (select chan1 send_req_exclusive$i)))))) l7)))
(assert (= l1 l4))
(assert (forall ((n node$type)) (or l4 (and (distinct (select shrset n) (z3name!0 n)) true))))
(assert (= l3 (= exclusive (c_state (select cache send_req_exclusive$i)))))
(assert (let (($x28 true))))
(assert l5)
(assert (= l6 (= n!3 auxnode)))
(assert (= l7 (= exgntd Truth)))
(assert l2)
(assert (= l9 (forall ((k!00 node$type)) (or (not l11) (= (z3name!0 k!00) Truth)))))
(assert (= l4 (forall ((k!00 node$type)) (or (= k!00 auxnode) (= (z3name!0 k!00) Falsity)))))
(assert l15)
(assert (= (forall ((n node$type)) (or l7 (= (select shrset n) (z3name!0 n)))) l8))
(assert (= l13 l0))
(assert (= l14 (= (select shrset n!1) z3name!2)))
(assert l16)
(assert (let (($x74 (not l7)))))
(assert (= l17 (= z3name!2 Truth)))
(assert (= l18 (and (distinct empty (m_cmd (select chan1 send_req_exclusive$i))))))
(assert (= l20 l6))
(assert l21)
(check-sat)

@rainoftime
Copy link
Contributor Author

SEGV at ./src/ast/euf/euf_enode.h:198

(set-option :smt.ematching false)
(declare-fun P (Int) Bool)
(declare-fun R (Int) Bool)
(declare-fun Q (Int) Bool)
(assert (and (forall ((x Int)) (R x)) (or (= P R) (and 
8000
(distinct Q R)))))
(check-sat)

@zhendongsu
Copy link

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 32 column 10: an invalid model was generated")
[530] % cat small.smt2
(declare-fun a () (Array Int Int))
(declare-fun b () Int)
(declare-fun r () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun s () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun t () Int)
(declare-fun u () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun v () Int)
(declare-fun i () Int)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n ((Array Int Int) (Array Int Int)) Int)
(assert (not (= k m)))
(assert (not (= k l)))
(assert (= g l))
(assert (not (= g g i)))
(assert (not (= g v)))
(assert (let ((o (store (store (store (store (store (store (store
  (store (store (store a g 1) v r) i c) w d) x s) j e) k f) l t) m u)
  h b))(p (store (store (store (store (store (store (store (store
  (store (store a k f) v r) j e) w d) h b) x s) m u) g 1) i c) l t)))
  (let ((q (n o p))) (not (= q (p q))))))
(check-sat)
[531] %

@zhendongsu
Copy link

Failed to verify:

[540] % z3release model_validate=true small.smt2
unsat
[541] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
failed to verify: (let ((a!1 (select (select (store ((as const (Array Int (Array Int Real)))
                                    (_ as-array k!8))
                                  (- 7719)
                                  (_ as-array k!7))
                           c!1)
                   b!0)))
  (= (= (ite (= (- 7719) b!0) 7719.0 7720.0) a!1) (<= c!1 e!4)))
evaluated to false
(params drat.file null keep_cardinality_constraints true pb.solver solver)
(= (- 7719) b!0) |-> 2
(= (ite (= (- 7719) b!0) 7719.0 7720.0) 7719.0) |-> 3
(= (ite (= (- 7719) b!0) 7719.0 7720.0) 7720.0) |-> 4
(let ((a!1 (select (select (store ((as const (Array Int (Array Int Real)))
                                    (_ as-array k!8))
                                  (- 7719)
                                  (_ as-array k!7))
                           c!1)
                   b!0)))
  (= (ite (= (- 7719) b!0) 7719.0 7720.0) a!1)) |-> 5
(<= c!1 e!4) |-> 6
(= (- 7719) c!1) |-> 7
(= (select (store ((as const (Array Int (Array Int Real))) (_ as-array k!8))
                  (- 7719)
                  (_ as-array k!7))
           c!1)
   (select ((as const (Array Int (Array Int Real))) (_ as-array k!8)) c!1)) |-> 8
false |-> 9
true |-> 10
[542] % 
[542] % cat small.smt2
(declare-fun a ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((b Int) (c Int) (d (Array Int (Array Int Real))) (g (Array Int (Array Int Real))) (e Int)) (let ((f (a d g))) (= (<= c e) (distinct (select (f b) c) (select (f c) b))))))
(check-sat)
[543] %

@zhendongsu
Copy link

SEGV ../src/sat/smt/arith_solver.cpp:626:

[509] % z3release small.smt2
sat
[510] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[511] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[512] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==29390==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000038 (pc 0x55d443cc403a bp 0x7ffec29e9a10 sp 0x7ffec29e9520 T0)
==29390==The signal is caused by a READ memory access.
==29390==Hint: address points to the zero page.
    #0 0x55d443cc4039 in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) ../src/sat/smt/arith_solver.cpp:626
    #1 0x55d443ca00df in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) ../src/sat/smt/euf_model.cpp:184
    #2 0x55d443ca612d in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:76
    #3 0x55d443c1439e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:123
    #4 0x55d443c15cb5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:216
    #5 0x55d444b1b6c8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #6 0x55d444ae62ae in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #7 0x55d444ae7c57 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:170
    #8 0x55d44494e7e8 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #9 0x55d4449718af in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #10 0x55d44498a2d4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #11 0x55d44495f6a6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #12 0x55d4448db1e5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #13 0x55d444835903 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #14 0x55d444835903 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #15 0x55d444835903 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #16 0x55d4447ea935 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #17 0x55d441b7443f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #18 0x55d441b1eee4 in main ../src/shell/main.cpp:371
    #19 0x7fc1ebda7b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #20 0x55d441b34be9 in _start (/local/suz-local/software/z3san/build-09022021112157-af5c6e4/z3+0x207be9)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/sat/smt/arith_solver.cpp:626 in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&)
==29390==ABORTING
[513] % 
[513] % cat small.smt2
(set-option :smt.arith.reflect false)
(assert (<= (* (* (* 0 0) 0) 0) 0))
(check-sat)
[514] %

@zhendongsu
Copy link

Solution unsoundness:

[521] % z3release small.smt2
unsat
[522] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[523] % cat small.smt2
(assert (<= (- 0 (- 1)) (ite (exists ((a Real)) (= a 0)) 0 1)))
(check-sat)
[524] %

@zhendongsu
Copy link

Invalid model:

[537] % z3release model_validate=true small.smt2
sat
[538] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 51 column 10: an invalid model was generated")
[539] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun d () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(declare-fun f () (_ BitVec 1))
(declare-fun x () (_ BitVec 1))
(declare-fun g () (_ BitVec 1))
(declare-fun h () (_ BitVec 1))
(declare-fun i () (_ BitVec 1))
(declare-fun j () (_ BitVec 1))
(declare-fun k () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun m () (_ BitVec 32))
(declare-fun n () (_ BitVec 32))
(declare-fun o () (_ BitVec 32))
(declare-fun p () (_ BitVec 32))
(declare-fun q () (_ BitVec 32))
(declare-fun r () (_ BitVec 32))
(declare-fun s () (_ BitVec 32))
(assert (let ((t (bvadd (_ bv3 32))) (u (bvadd (_ bv2 32)))(v (bvadd
    (_ bv134540500 32)))(w (bvadd (_ bv134540500 32)))) (= (ite (= j
    (ite (= k l) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand
    (ite (= i (ite (= l (bvor (bvor (bvor (concat (_ bv0 24) (select c
    (bvadd n))) (bvshl (concat (_ bv0 24) (select c (bvadd n (_ bv1
    32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvadd
    n))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c (bvadd n (_
    bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (ite (= h (ite (=
    c (store (store (store (store b t ((_ extract 7 0) (bvlshr m (_
    bv24 32)))) u ((_ extract 7 0) (bvlshr m (_ bv16 32)))) v ((_
    extract 7 0) (bvlshr m (_ bv8 32)))) w ((_ extract 7 0) m))) (_
    bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= g (ite (= m
    (bvadd p (_ bv1 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))
    (bvand (ite (= x (ite (= n o) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_
    bv0 1)) (bvand (ite (= f (ite (= b (store (store (store (store a
    (bvadd o (_ bv3 32)) ((_ extract 7 0) (bvand r (_ bv24 32))))
    (bvadd o (_ bv2 32)) ((_ extract 7 0) (bvlshr r (_ bv16 32))))
    (bvadd (_ bv1 32)) ((_ extract 7 0) (bvlshr r (_ bv8 32)))) o ((_
    extract 7 0) r))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))
    (bvand (ite (= e (ite (= o (bvsub s (_ bv4 32))) (_ bv1 1) (_ bv0
    1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= d (ite (= p (bvor (bvor
    (bvor (bvshl (concat (_ bv0 24) (select a v)) (_ bv8 32))))
    (bvxnor (concat (_ bv0 24) (select a t)) (_ bv24 32)))) (_ bv1 1)
    (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (distinct (ite (= q (bvor
    (bvor (bvor (concat (_ bv0 24) (select a (bvadd s (_ bv0 32))))
    (bvshl (concat (_ bv0 24) (select a s)) (_ bv8 32))) (bvshl
    (concat (_ bv0 24) (select a (bvadd s (_ bv2 32)))) (_ bv16
    32))(concat (_ bv0 24) (select a (bvadd s (_ bv3 32)))) (_ bv24
    32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))))(bvnot (_
    bv0 1)))))
(check-sat)
[540] %

@zhendongsu
Copy link

SEGV ../src/ast/ast.h:501:

[573] % z3release small.smt2
sat
[574] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[575] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[576] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==25176==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x5603fb05a0bb bp 0x7ffdbadbc480 sp 0x7ffdbadbc480 T0)
==25176==The signal is caused by a READ memory access.
==25176==Hint: address points to the zero page.
    #0 0x5603fb05a0ba in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x5603fb05a0ba in expr::get_sort() const ../src/ast/ast.cpp:406
    #2 0x5603fb067ed5 in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2111
    #3 0x5603fb093753 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2152
    #4 0x5603fb083558 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2266
    #5 0x5603f8e401df in arith::solver::add_value(euf::enode*, model&, ref_vector<expr, ast_manager>&) ../src/sat/smt/arith_solver.cpp:628
    #6 0x5603f8e1c0df in euf::solver::dependencies2values(euf::solver::user_sort&, top_sort<euf::enode>&, ref<model>&) ../src/sat/smt/euf_model.cpp:184
    #7 0x5603f8e2212d in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:76
    #8 0x5603f8d9039e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:123
    #9 0x5603f8d91cb5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:216
    #10 0x5603f9c976c8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #11 0x5603f9c622ae in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #12 0x5603f9c63c57 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:170
    #13 0x5603f9aca7e8 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #14 0x5603f9aed8af in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #15 0x5603f9b062d4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #16 0x5603f9adb6a6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #17 0x5603f9a571e5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #18 0x5603f99b1903 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #19 0x5603f99b1903 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #20 0x5603f99b1903 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #21 0x5603f9966935 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #22 0x5603f6cf043f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #23 0x5603f6c9aee4 in main ../src/shell/main.cpp:371
    #24 0x7fde196bdb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #25 0x5603f6cb0be9 in _start (/local/suz-local/software/z3san/build-09022021112157-af5c6e4/z3+0x207be9)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
==25176==ABORTING
[577] % 
[577] % cat small.smt2
(set-option :smt.arith.reflect false)
(declare-const a Int)
(assert (<= (+ (* (- 3 2) a)) 0))
(check-sat)
[578] %

@zhendongsu
Copy link

Invalid model (might be related to #5532 (comment)):

[515] % z3release model_validate=true small.smt2
sat
[516] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 18 column 10: an invalid model was generated")
[517] % cat small.smt2
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun f () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun e () (_ BitVec 32))
(declare-fun h () (_ BitVec 32))
(declare-fun g () (_  BitVec 1))
(assert (= (ite (= g (ite (= f (store (store (store (store d (bvadd (_
   bv3 32)) ((_ extract 7 0) (bvlshr e (_ bv24 32)))) (bvadd (_ bv2
   32)) ((_ extract 7 0) (bvlshr e (_ bv16 32)))) a ((_ extract 7 0)
   (bvlshr e (_ bv8 32)))) (bvadd a) ((_ extract 7 0) e))) (_ bv1 1)
   (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= d (store (store (store
   (store c (bvadd b (_ bv3 32)) ((_ extract 7 0) (bvlshr h (_ bv24
   32)))) (bvadd (_ bv2 32)) ((_ extract 7 0) (bvlshr h (_ bv16 32))))
   b ((_ extract 7 0) (bvlshr h (_ bv8 32)))) (bvadd (_ bv0 32)) ((_
   extract 7 0) h))) (_ bv1 1) (_ bv0 1))))
(check-sat)
[518] %

NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
c4158eb
NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
87f5b92
NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
a566c73
NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
5633af7
NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
0ddbbe9
NikolajBjorner added a commit that referenced this issue Sep 3, 2021
@NikolajBjorner
#5532
cdcfbeb 
remove "reflect" parameter from exposed options. It should be internal only.
@NikolajBjorner
Copy link
Contributor
NikolajBjorner commented Sep 3, 2021 •
edited
Loading

arith.reflect is really an internal parameter. I hid it. The bug was also fixed.

@zhendongsu
Copy link

Assertion violation:

[530] % z3release small.smt2
sat
[531] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 346
Failed to verify: !was_eliminated(lits[i])

Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[532] % 
[532] % cat small.smt2
(set-option :sat.core.minimize true)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun g () (_ BitVec 32))
(define-fun d () Bool (= true (let ((e (= true (= true (= true (= true
   (= true (> 0)))))))) (let ((f (= true (= true (=(= b g) e))))) (=
   true (=> (= g (bvadd (bvmul a c))) true f))))))
(assert (not (=> (ite d (ite (ite d (not (=> true d)) (=> true (=> (=>
   true d) (not (=> true d))))) (ite d (not (=> true d)) (=> true (=>
   (=> true d) (not (=> true d))))) (ite d (not (=> true d)) (=> true
   (=> (=> true d) (not (=> true d)))))) (ite (ite d (not (=> true d))
   (=> true (=> (=> true d) (not (=> true d))))) (ite d (not (=> true
   d)) (=> true (=> (=> true d) (not (=> true d))))) (ite d (not (=>
   true d)) (=> true (=> (=> true d) (not (=> true d))))))) d)))
(check-sat)
[533] %

@zhendongsu
Copy link

SEGV ../src/ast/ast.h:501:

[578] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[579] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[580] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==24406==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x563afdb28a8b bp 0x7f59099b9a40 sp 0x7f59099b9a40 T10)
==24406==The signal is caused by a READ memory access.
==24406==Hint: address points to the zero page.
ASAN:DEADLYSIGNAL
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
ASAN:DEADLYSIGNAL
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
ASAN:DEADLYSIGNAL
==24406==AddressSanitizer: while reporting a bug found another one. Ignoring.
    #0 0x563afdb28a8a in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x563afdb28a8a in expr::get_sort() const ../src/ast/ast.cpp:406
    #2 0x563afdb36a71 in ast_manager::check_args(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2202
    #3 0x563afdb62444 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2164
    #4 0x563afdb51f28 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2266
    #5 0x563afdb61238 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1943
    #6 0x563afdb61238 in ast_manager::mk_app(int, int, expr*, expr*, expr*) ../src/ast/ast.cpp:1962
    #7 0x563afbb9b1b9 in ast_manager::mk_ite(expr*, expr*, expr*) ../src/ast/ast.h:2128
    #8 0x563afbb9b1b9 in bv::solver::assert_bv2int_axiom(app*) ../src/sat/smt/bv_internalize.cpp:425
    #9 0x563afbbad3be in bv::solver::internalize_bv2int(app*) ../src/sat/smt/bv_internalize.cpp:405
    #10 0x563afbbad3be in bv::solver::internalize_circuit(app*) ../src/sat/smt/bv_internalize.cpp:219
    #11 0x563afbbb3932 in bv::solver::post_visit(expr*, bool, bool) ../src/sat/smt/bv_internalize.cpp:150
    #12 0x563afbafd0e0 in euf::th_internalizer::visit_rec(ast_manager&, expr*, bool, bool, bool) ../src/sat/smt/sat_th.cpp:48
    #13 0x563afb896413 in euf::solver::internalize(expr*, bool) ../src/sat/smt/euf_internalize.cpp:29
    #14 0x563afb896413 in euf::solver::e_internalize(expr*) ../src/sat/smt/euf_internalize.cpp:426
    #15 0x563afb9eaa9e in arith::solver::mk_enode(expr*) ../src/sat/smt/arith_internalize.cpp:567
    #16 0x563afb9eb1c4 in arith::solver::mk_evar(expr*) ../src/sat/smt/arith_internalize.cpp:580
    #17 0x563afba066db in arith::solver::linearize(arith::solver::scoped_internalize_state&) ../src/sat/smt/arith_internalize.cpp:283
    #18 0x563afba0c86c in arith::solver::linearize_term(expr*, arith::solver::scoped_internalize_state&) ../src/sat/smt/arith_internalize.cpp:149
    #19 0x563afb9fdfc3 in arith::solver::internalize_def(expr*) ../src/sat/smt/arith_internalize.cpp:416
    #20 0x563afba15032 in arith::solver::internalize_atom(expr*) ../src/sat/smt/arith_internalize.cpp:339
    #21 0x563afba18778 in non-virtual thunk to arith::solver::internalize(expr*, bool, bool, bool) (/local/suz-local/software/z3san/build-09032021174236-18e4546/z3+0x249e778)
    #22 0x563afb8957f4 in euf::solver::internalize(expr*, bool, bool, bool) ../src/sat/smt/euf_internalize.cpp:62
    #23 0x563afb845ce9 in goal2sat::imp::convert_euf(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:676
    #24 0x563afb84cadd in goal2sat::imp::convert_atom(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:303
    #25 0x563afb84dd60 in goal2sat::imp::visit(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:399
    #26 0x563afb84e84f in goal2sat::imp::process(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:778
    #27 0x563afb855cf2 in goal2sat::imp::process(expr*) ../src/sat/tactic/goal2sat.cpp:875
    #28 0x563afb855cf2 in goal2sat::imp::operator()(goal const&) ../src/sat/tactic/goal2sat.cpp:944
    #29 0x563afa678c15 in inc_sat_solver::internalize_goal(ref<goal>&) ../src/sat/sat_solver/inc_sat_solver.cpp:738
    #30 0x563afa67a69e in inc_sat_solver::internalize_formulas() ../src/sat/sat_solver/inc_sat_solver.cpp:906
    #31 0x563afa682193 in inc_sat_solver::check_sat_core(unsigned int, expr* const*) ../src/sat/sat_solver/inc_sat_solver.cpp:205
    #32 0x563afc5bc2df in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #33 0x563afa644614 in pb2bv_solver::check_sat_core2(unsigned int, expr* const*) ../src/tactic/fd_solver/pb2bv_solver.cpp:80
    #34 0x563afc5bc2df in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #35 0x563afc5bc2df in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #36 0x563afc5aa0d6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #37 0x563afc617ed0 in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:160
    #38 0x563afc617ed0 in parallel_tactic::solver_state::simplify() ../src/solver/parallel_tactic.cpp:281
    #39 0x563afc617ed0 in parallel_tactic::cube_and_conquer(parallel_tactic::solver_state&) ../src/solver/parallel_tactic.cpp:519
    #40 0x563afc61fddc in parallel_tactic::run_solver() ../src/solver/parallel_tactic.cpp:672
    #41 0x7f59252bf6de  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd6de)
    #42 0x7f59255926da in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76da)
    #43 0x7f592497ca3e in __clone (/lib/x86_64-linux-gnu/libc.so.6+0x121a3e)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
Thread T10 created by T0 here:
    #0 0x7f59257e1d2f in __interceptor_pthread_create (/usr/lib/x86_64-linux-gnu/libasan.so.4+0x37d2f)
    #1 0x7f59252bf994 in std::thread::_M_start_thread(std::unique_ptr<std::thread::_State, std::default_delete<std::thread::_State> >, void (*)()) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xbd994)
    #2 0x563afc7721d5 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:119
    #3 0x563afc730cde in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #4 0x563afc732687 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:170
    #5 0x563afc4b3ce3 in check_sat_using_tactic_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:216
    #6 0x563afc47baf8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2906
    #7 0x563afc4801bc in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3012
    #8 0x563afc4801bc in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #9 0x563afc435365 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #10 0x563af97c113f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #11 0x563af976bc14 in main ../src/shell/main.cpp:371
    #12 0x7f592487cb96 in __libc_start_main
67E6
 (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)

==24406==ABORTING
[581] % 
[581] % cat small.smt2
(set-option :sat.prob_search true)
(set-option :parallel.enable true)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= (div 0 a) b))
(check-sat-using (then purify-arith qffd))
[582] %

@zhendongsu
Copy link

Invalid model (might be related to #5532 (comment)):

[566] % z3release model_validate=true small.smt2
sat
[567] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 32 column 10: an invalid model was generated")
[568] % 
[568] % cat small.smt2
(declare-fun a () (Array Int Int))
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun w () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun x () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun s () Int)
(declare-fun sk ((Array Int Int) (Array Int Int)) Int)
(assert (let ((t (store (store (store (store (store (store (store
   (store (store (store (store (store (store (store (store (store
   (store (store (store (store a 1 b) 2 k) 3 m) 4 n) 5 o) 6 p) 23 q) 8
   r) 9 s) 10 c) 11 d) 12 w) 13 e) 72 f) 15 x) 16 g) 17 h) 18 i) 19 j)
   20 l)) (u (store (store (store (store (store (store (store (store
   (store (store (store (store (store (store (store (store (store
   (store (store (store a 46 s) 2 2) 4 4) 93 k) 2 1) 19 j) 1 1) 8 8)
   15 x) 10 c) 6 6) 14 f) 3 3) 16 g) 82 o) 18 i) 7 7) 20 l) 3 3) 17
   h))) (let ((v (sk t u))) (not (= (t v) (u v))))))
(check-sat)
[569] %

@zhendongsu
Copy link

Assertion violation:

[580] % z3debug small.smt2
sat
[581] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/euf/euf_etable.cpp
Line: 75
arity >= d->get_arity() || d->is_associative()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[582] % cat small.smt2
(assert (= 0 (div 0)))
(check-sat)
[583] %

@zhendongsu
Copy link

Assertion violation:

[590] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast_translation.h
Line: 79
!n || from().contains(const_cast<T*>(n))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/ast/ast_translation.h
Line: 79
!n || from().contains(const_cast<T*>(n))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/ast/ast_translation.h
Line: 79
!n || from().contains(const_cast<T*>(n))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
ASSERTION VIOLATION
File: ../src/ast/ast_translation.h
Line: 79
!n || from().contains(const_cast<T*>(n))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[591] % cat small.smt2
(set-option :sat.prob_search true)
(set-option :parallel.enable true)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((b (concat (select a (_ bv10 32)) (concat (select a (_
   bv9 32)) (select a (_ bv8 32)))))) (let ((c (concat (select a (_
   bv13 32)) (concat (select a (_ bv12 32)) (concat (select a (_ bv11
   32)) b))))) (let ((d ((_ to_fp 11 53) (concat (select a (_ bv15
   32)) (concat (select a (_ bv14 32)) c))))) (fp.isNaN d)))))
(check-sat-using qffd)
[592] %

@zhendongsu
Copy link

Invalid model:

[523] % z3release model_validate=true small.smt2
sat
[524] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 22 column 22: an invalid model was generated")
[525] % 
[525] % cat small.smt2
(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(declare-fun c () (Array Int Int))
(declare-fun d () (Array Int Int))
(declare-fun e () (Array Int Int))
(declare-fun f () (Array Int Int))
(declare-fun n () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun l () (Array Int Int))
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun o () Int)
(declare-fun m ((Array Int Int) (Array Int Int)) Int)
(assert (= (store l k n) (store b k i)))
(assert (= c d (store a j h)))
(assert (distinct e (store d o g)))
(assert (= n (select a j)))
(assert (distinct h (select a o) (select b o)))
(assert (= k (select e (m c f))))
(check-sat-using qfidl)
[526] %

NikolajBjorner added a commit that referenced this issue Sep 4, 2021
@NikolajBjorner
#5532
9c5ef79
NikolajBjorner added a commit that referenced this issue Sep 4, 2021
@NikolajBjorner
#5532
051ede6
NikolajBjorner added a commit that referenced this issue Sep 5, 2021
@NikolajBjorner
#5532
9c91698
NikolajBjorner added a commit that referenced this issue Sep 5, 2021
@NikolajBjorner
#5532
3021da8
NikolajBjorner added a commit that referenced this issue Sep 5, 2021
@NikolajBjorner
#5532
3764eb1 
ensure re-internalization for predicates that are replayed.
Theory internalization is currently not considered in depth.
@zhendongsu
Copy link

Assertion violation:

[590] % z3release small.smt2
sat
[591] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/subpaving/tactic/expr2subpaving.cpp
Line: 328
UNEXPECTED CODE WAS REACHED.
Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[592] % 
[592] % cat small.smt2
(set-option :rewriter.arith_ineq_lhs true)
(set-option :sat.prob_search true)
(set-option :rewriter.sort_sums true)
(declare-fun a () Real)
(assert (distinct 0 (/ a (div (to_int a) 10))))
(check-sat-using (then purify-arith smt subpaving))
[593] %

@zhendongsu
Copy link

Assertion violation:

[600] % z3release small.smt2
unknown
[601] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 151
UNEXPECTED CODE WAS REACHED.
Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[602] % 
[602] % cat small.smt2
(set-option :smt.mbqi false)
(set-option :parallel.enable true)
(declare-fun a () (Array Int Int))
(assert (forall ((b Int)) (=> (< 0 b) (exists ((c Int)) (let ((d (store (store a 0 0) 10 0))) (= c (d b)))))))
(check-sat-using qffd)
[603] %

@zhendongsu
Copy link

Assertion violation:

[589] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unknown
[590] % 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
[591] % cat small.smt2
(set-option :sat.prob_search true)
(set-option :parallel.enable true)
(declare-fun a () Int)
(assert (= (div a 2) 0))
(check-sat-using (then purify-arith add-bounds qffd))
[592] %

@NikolajBjorner
Copy link
Contributor

Note that parallel search requires copying the solver state around. This code path is not well tested yet, but not too relevant for sequential mode. Therefore, if you start setting parallel.enable=true you are likely (as demonstrated) to produce more crashes. I might be able to investigate based on running with the parallel mode on, but setting up self-contained unit testing is going to be easier to work with to start with.
There are still several bugs in sequential mode that have much higher priority
so maybe dampen the enthusiasm for parallel at this point.

@zhendongsu
Copy link

Assertion violation:

[573] % z3debug small.smt2
unknown
[574] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
...
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 605
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[575] % cat small.smt2
(declare-fun trans ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun a ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((b Int) (c Int) (d Int) (k Int) (e (Array Int (Array Int Real))) (f (Array Int (Array Int Real))) (l Int))
   (let ((g (a e (a f (trans e))))) (= (= (select (f d) k) 0) (distinct 0 (select (g c) b))))))
(assert (forall ((h Int) (i Int) (j (Array Int (Array Int Real)))) (let ((g (trans j))) (= 0 (select (g i) h)))))
(check-sat)
[576] %

NikolajBjorner added a commit that referenced this issue Sep 6, 2021
@NikolajBjorner
#5532
72f6271 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
NikolajBjorner added a commit that referenced this issue Sep 7, 2021
@NikolajBjorner
#5532 remove unsound rewrite rule that was recently added
be4df46
NikolajBjorner added a commit that referenced this issue Sep 7, 2021
@NikolajBjorner
left over bugs #5532
9341574 
disabling complete const rewriting (temporarily) as it can loop
NikolajBjorner added a commit that referenced this issue Sep 7, 2021
@NikolajBjorner
#5532 add blocking condition for recursion.
8c406c1
NikolajBjorner added a commit that referenced this issue Sep 8, 2021
@NikolajBjorner
#5532
c4d0ded
@zhendongsu
Copy link

Assertion violation:

[544] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 651
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[545] % cat small.smt2
(set-option :sat.prob_search true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= (= (/ (+ a a) 0) (/ b 0)) (= a 1)))
(check-sat-using (then smt qfnra qe2))
[546] %

@zhendongsu
Copy link

Assertion violation:

[540] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_arith.cpp
Line: 72
m.limit().is_canceled() || !m.is_false(val)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[541] % 
[541] % cat small.smt2
(declare-fun a (Real) (Array Int (Array Int Real)))
(assert (forall ((b Int) (c Int) (d Real)) (and (= (select (select (a d) b) c) d))))
(check-sat)
[542] %

@zhendongsu
Copy link

Assertion violation:

[532] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
...
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 615
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[533] % cat small.smt2
(declare-fun a () Real)
(declare-fun f () Int)
(declare-fun b (Real) (Array Int (Array Int Real)))
(assert (forall ((c Int) (d Int) (g Int) (e Real)) (= (<= d g) (= (select (select (b e) c) d) e))))
(assert (not (= (and true) (forall ((h Int)) (= (<= h f) (= 0 a))))))
(check-sat)
[534] %

@zhendongsu
Copy link

Assertion violation:

[554] % z3debug small.smt2
unsat
[555] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
set bool_var 35: (forall (vars (d Real)) (= (and #30) (< (:var 0) b)))
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1184
m_columns_with_changed_bounds.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[556] % cat small.smt2
(declare-fun a ()  Real)
(declare-fun b ()  Real)
(declare-fun c ()  Real)
(assert (forall ((d Real)) (= (and (xor (= c (+ (mod a 0))) true)) (< d b))))
(check-sat)
[557] %

@zhendongsu
Copy link

SEGV ../src/sat/smt/dt_solver.cpp:718:

[545] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
set bool_var 28: (forall (vars (i c)) (distinct (= #24 b)))
set bool_var 34: (forall (vars (i c)) (= (f #30) invack))
ASAN:DEADLYSIGNAL
=================================================================
==15021==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000070 (pc 0x5577b59bd86b bp 0x7fff75b97f10 sp 0x7fff75b97cf0 T0)
==15021==The signal is caused by a READ memory access.
==15021==Hint: address points to the zero page.
    #0 0x5577b59bd86a in dt::solver::add_dep(euf::enode*, top_sort<euf::enode>&) ../src/sat/smt/dt_solver.cpp:718
    #1 0x5577b58840d3 in euf::solver::collect_dependencies(euf::solver::user_sort&, top_sort<euf::enode>&) ../src/sat/smt/euf_model.cpp:103
    #2 0x5577b58900be in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:74
    #3 0x5577b5a96279 in q::mbqi::init_model() ../src/sat/smt/q_mbi.cpp:563
    #4 0x5577b5a96279 in q::mbqi::operator()() ../src/sat/smt/q_mbi.cpp:56
    #5 0x5577b584b4af in q::solver::check() ../src/sat/smt/q_solver.cpp:76
    #6 0x5577b580a72a in operator() ../src/sat/smt/euf_solver.cpp:465
    #7 0x5577b580a72a in euf::solver::check() ../src/sat/smt/euf_solver.cpp:483
    #8 0x5577b75f6d9c in sat::solver::final_check() ../src/sat/sat_solver.cpp:1755
    #9 0x5577b761fa17 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1730
    #10 0x5577b7620281 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1717
    #11 0x5577b762139f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1343
    #12 0x5577b57f7cda in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:72
    #13 0x5577b57fbfc5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:216
    #14 0x5577b6709278 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #15 0x5577b66d418e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #16 0x5577b66d5b37 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:170
    #17 0x5577b653c6a8 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #18 0x5577b655f76f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #19 0x5577b6578194 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #20 0x5577b654d566 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:317
    #21 0x5577b64c9055 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #22 0x5577b6423743 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #23 0x5577b6423743 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #24 0x5577b6423743 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3158
    #25 0x5577b63d8705 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3207
    #26 0x5577b375b84f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #27 0x5577b3706324 in main ../src/shell/main.cpp:371
    #28 0x7f69e3ddab96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #29 0x5577b371c029 in _start (/local/suz-local/software/z3san/build-09102021070904-34f878f/z3+0x208029)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/sat/smt/dt_solver.cpp:718 in dt::solver::add_dep(euf::enode*, top_sort<euf::enode>&)
==15021==ABORTING
[546] %
[546] % cat small.smt2
(declare-datatypes ((a 0)) (((b))))
(declare-sort c)
(declare-datatypes ((d 0)) (((empty) (invack))))
(declare-datatypes ((e 0)) (((j (f d)))))
(declare-fun g () (Array c a))
(declare-fun h () (Array c e))
(assert (xor (forall ((i c)) (distinct (= (select g i) b))) (forall ((i c)) (= (f (select h i)) invack))))
(check-sat)
[547] %

@zhendongsu
Copy link

Assertion violation:

[567] % z3debug small.smt2
unsat
[568] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
set bool_var 38: (forall (vars (d Real)) (and (distinct b #30) (and #33 #35)))
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 635
"integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[569] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ((d Real)) (and (distinct b (mod 0 (div c a))) (= d a 7))))
(check-sat)
[570] %

@zhendongsu
Copy link

Assertion violation:

[511] % z3debug small.smt2
unsat
[512] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
set bool_var 34: (forall (vars (i Real) (j c)) (= (to_real 0) (d e #30)))
set bool_var 40: (< (d e (to_real 0)) 1.0)
set bool_var 53: (forall (vars (i Real)) (= (d h #49) (* (:var 0))))
set bool_var 59: (forall (vars (i Real)) (= (to_real 0) (/ #56)))
set bool_var 90: (= i!2 0.0)
set bool_var 128: (= j!3 c!val!0)
set bool_var 129: (<= 0.0 i!2)
set bool_var 122: (= (if (<= 0.0 i!2) 0.0 -38.0) 0.0)
set bool_var 130: (= (if (<= 0.0 i!2) 0.0 -38.0) -38.0)
set bool_var 132: (= 0.0 (if (<= 0.0 i!2) 0.0 -38.0))
set bool_var 128: (= j!3 c!val!0)
set bool_var 129: (<= 0.0 i!2)
set bool_var 122: (= (if (<= 0.0 i!2) 0.0 -38.0) 0.0)
set bool_var 130: (= (if (<= 0.0 i!2) 0.0 -38.0) -38.0)
set bool_var 132: (= 0.0 (if (<= 0.0 i!2) 0.0 -38.0))
set bool_var 2: false
set bool_var 136: (= i!2 -3.0)
set bool_var 140: (= i!2 0.0)
set bool_var 128: (= j!3 c!val!0)
set bool_var 129: (<= 0.0 i!2)
set bool_var 122: (= (if (<= 0.0 i!2) 0.0 -38.0) 0.0)
set bool_var 130: (= (if (<= 0.0 i!2) 0.0 -38.0) -38.0)
set bool_var 132: (= 0.0 (if (<= 0.0 i!2) 0.0 -38.0))
set bool_var 2: false
set bool_var 136: (= i!2 -3.0)
set bool_var 140: (= i!2 0.0)
set bool_var 79: (= 0.0 i!2)
ASSERTION VIOLATION
File: ../src/ast/euf/euf_enode.h
Line: 158
i < num_args()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[513] % cat small.smt2
(declare-sort a)
(declare-sort b)
(declare-sort c)
(declare-fun d (a Real) Real)
(declare-fun e () a)
(declare-fun f (b c) Real)
(declare-fun g () b)
(declare-fun h () a)
(assert (forall ((i Real) (j c)) (= 0 (d e (+ i (/ (* (f g j)) 1.0))))))
(assert (< (d e 0) 1.0))
(assert (forall ((i Real)) (= (d h (* 2.0 i)) (* i))))
(assert (forall ((i Real)) (= 0 (/ (d h i)))))
(check-sat)
[514] %

@zhendongsu
Copy link

Refutation unsoundness:

[586] % z3release small.smt2
sat
[587] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[588] % cat small.smt2
(set-option :sat.minimize_lemmas false)
(set-option :nlsat.inline_vars true)
(set-option :smt.arith.nl.grobner false)
(declare-fun a () Real)
(assert (= (/ a (* a (* a a (* (* a a) a))) (* a (* a a (* (* a a) a)))) (* 2 2 2)))
(check-sat)
[589] %

@zhendongsu
Copy link
zhendongsu commented Sep 14, 2021 •
edited by NikolajBjorner
Loading

Refutation unsoundness:

[532] % z3release small.smt2
sat
[533] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[534] % cat small.smt2
(set-option :rewriter.flat false)
(set-option :nlsat.inline_vars true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (=> (and (> (* (- (* a a)) (- b (* a a))) (+ a (* (* a a) b))
  (* (- (* a a)) (- b (* a a)))) (= b (+ (- (* (- (+ a (* a (* (ite (<
  1 b) b b) a))) (+ a (* a (* (ite (< 1 b) b b) a)))) (+ a (* a (- (+
  a (* a a))))) b (- (+ a (* a (* (ite (< 1 b) b b) a))) (+ a (* a (*
  (ite (< 1 b) b b) a)))))) (* a (* (+ a (* a (/ a b))) (* a a)) (* a
  a))))) (and (> (+ a (* (* a a) b)) (* (- (* a a)) (- b (* a a))) (+
  a (* (* a a) b))) (= b (+ (- (* (- (+ a (* a (* (ite (< 1 b) b b)
  a))) (+ a (* a (* (ite (< 1 b) b b) a)))) (+ a (* a (- (+ a (* a
  a))))) b (- (+ a (* a (* (ite (< 1 b) b b) a))) (+ a (* a (* (ite (<
  1 b) b b) a))))) (* (+ a (* a (/ a b))) (* a a)) (* a a))))) (and (>
  (+ a (* (* a)) 0) (+ a (* (* a a) b))))))
(check-sat)
[535] %

I will go over other above, but skip the NLSAT related bugs. The root cause is almost for sure outside of the new code and related to already filed bugs. Root causing nlsat related bugs for the new code is double overhead.

NikolajBjorner added a commit that referenced this issue Sep 20, 2021
@NikolajBjorner
#5532
0170f1f
NikolajBjorner added a commit that referenced this issue Sep 20, 2021
@NikolajBjorner
#5532
1352aa0
@NikolajBjorner
Copy link
Contributor

a few of these come from the same regression introduced a few days before filing.

remaining two sad faces are probably more difficult so focus is on those, but context switching with polysat branch also this week.

one of the parallel.enable bugs was fixed, but others have different root causes.

the nlsat (non-linear bugs) have already simpler repros in long standing open bugs independent of sat.euf.

NikolajBjorner added a commit that referenced this issue Sep 22, 2021
@NikolajBjorner
#5532
cabd5b1
NikolajBjorner added a commit that referenced this issue Sep 22, 2021
@NikolajBjorner
#5532
18d1b36
NikolajBjorner added a commit that referenced this issue Sep 22, 2021
@NikolajBjorner
#5532
d174f87
@NikolajBjorner
Copy link
Contributor

one of the remaining bugs exposed a subtle miss for internalization

the parallel.enable bugs pointed to basic mixups in solver copy functionality.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@rainoftime @NikolajBjorner @zhendongsu
0