search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

[Consolidated] soundness issues, invalid models, and crashes for options "tactic.default_tactic=smt sat.euf=true" #5223

Closed zhendongsu closed 3 years ago

zhendongsu commented 3 years ago

Commit: https://github.com/Z3Prover/z3/commit/30e904bfa4ce7370b359a91ab9ab4c94bd6ee94a

[518] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[519] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[520] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==21324==ERROR: AddressSanitizer: SEGV on unknown address 0x000000001012 (pc 0x564e88cd99b1 bp 0x7fff10ce6180 sp 0x7fff10ce5f80 T0)
==21324==The signal is caused by a READ memory access.
    #0 0x564e88cd99b0 in euf::enode::hash() const ../src/ast/euf/euf_enode.h:167
    #1 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x564e88cd99b0 in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::insert(obj_map<euf::enode, euf::enode*>::key_data&&) ../src/util/hashtable.h:403
    #4 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::insert(euf::enode*, euf::enode* const&) ../src/util/obj_hashtable.h:141
    #5 0x564e88cd99b0 in dt::solver::occurs_check_enter(euf::enode*) ../src/sat/smt/dt_solver.cpp:589
    #6 0x564e88cdb477 in dt::solver::occurs_check(euf::enode*) ../src/sat/smt/dt_solver.cpp:637
    #7 0x564e88cdc55c in dt::solver::check() ../src/sat/smt/dt_solver.cpp:667
    #8 0x564e88b1c6ca in euf::solver::check() ../src/sat/smt/euf_solver.cpp:457
    #9 0x564e8a8c52dc in sat::solver::final_check() ../src/sat/sat_solver.cpp:1752
    #10 0x564e8a8ececf in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1727
    #11 0x564e8a8edd01 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1714
    #12 0x564e8a8eee1f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1341
    #13 0x564e88b0ba62 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:66
    #14 0x564e88b0f1c5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #15 0x564e89a033e8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #16 0x564e899cdfce in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #17 0x564e899cf977 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
    #18 0x564e89824730 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #19 0x564e89847d2f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #20 0x564e89860774 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #21 0x564e898356e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #22 0x564e897b77d5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1623
    #23 0x564e8970e823 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2605
    #24 0x564e8970e823 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2947
    #25 0x564e8970e823 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #26 0x564e896c3f55 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #27 0x564e86a5396f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #28 0x564e869fe357 in main ../src/shell/main.cpp:372
    #29 0x7fdab5d54b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #30 0x564e86a14109 in _start (/local/suz-local/software/z3san/build-04272021214656-30e904b/z3+0x206109)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_enode.h:167 in euf::enode::hash() const
==21324==ABORTING
[521] % 
[521] % cat small.smt2
(declare-datatypes ((a 0) (b 0) (c 0)) (((d)) ((cons (car c) (cdr b)) (e)) ((f (children b)))))
(declare-fun g () b)
(declare-fun h () b)
(declare-fun i () b)
(assert (or (and (or (or true (and ((_ is cons) (ite ((_ is cons) h) (cdr h) e)))) (distinct (ite ((_ is f) (f g)) (children (f g)) e) i)))))
(check-sat)
[522] %
zhendongsu commented 3 years ago 
[532] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 2360
ax_is_correct()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[533] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 41: (= a (+ e (* 2 #38))) false
31: a
0
40: (+ e (* 2 (f 0)))
(- 1)
sat
(error "line 8 column 10: an invalid model was generated")
[534] % 
[534] % 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) Int)
(assert (= (= d 43) (xor (and (= b e (- b d)) (>= a b)) (< c 0) (= a (+ e (* 2 (f 0)))) false false (= a b))))
(check-sat)
[535] %
zhendongsu commented 3 years ago 
[553] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 62: (= a 12) true
sat
(error "line 10 column 10: an invalid model was generated")
[554] % 
[554] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(assert (<= 0 a d))
(assert (< 17 (- c 1)))
(assert (< a (- c 4)))
(assert (= (= a 0) (= a 1) (= a 12) (= (b 7) e)))
(check-sat)
[555] %
zhendongsu commented 3 years ago 
[579] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 34: (= c (+ (* 2 #26) (* 2 #28) 0 55)) false
23: c
0
32: (+ (* 2 (g a)) (* 2 (e a)) 0 55)
(- 1)
sat
(error "line 7 column 10: an invalid model was generated")
[580] % 
[580] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun g (Int) Int)
(declare-fun e (Int) Int)
(assert (= b c (+ (* 2 (g a)) (* 2 (e a)) 0 55)))
(check-sat)
[581] %
zhendongsu commented 3 years ago 
[587] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 32: (= (bvand bv[0:1]) (bvxnor (if #29 bv[1:1] bv[0:1]) bv[1:1] bv[0:1])) false
22: (bvand bv[0:1])
#b0
31: (bvxnor (if (= a #28) bv[1:1] bv[0:1]) bv[1:1] bv[0:1])
#b1
sat
(error "line 9 column 10: an invalid model was generated")
[588] % 
[588] % cat small.smt2
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(assert
 (= (bvand (_ bv0 1))
  (bvxnor (ite (= a (ite (= b c) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))
   (_ bv1 1)
   (_ bv0 1))))
(check-sat)
[589] %
zhendongsu commented 3 years ago 
[643] % z3release small.smt2
sat
[644] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[645] % 
[645] % cat small.smt2
(declare-const a Int)
(assert (> a 0))
(assert (= (< a 0) false))
(check-sat)
[646] %
zhendongsu commented 3 years ago 
[676] % z3release small.smt2 
sat
[677] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[678] % 
[678] % cat small.smt2 
(assert (<= 1 (+ 1 0)))
(check-sat)
[679] %
zhendongsu commented 3 years ago 
[691] % z3release small.smt2
sat
[692] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[693] % 
[693] % cat small.smt2
(assert (or (< 0 1) (> 0 1)))
(check-sat)
[694] %
zhendongsu commented 3 years ago 
[723] % z3release small.smt2
sat
[724] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[725] % cat small.smt2
(declare-fun a () Bool)
(assert (not (exists ((b Bool)) a)))
(check-sat)
[726] %
zhendongsu commented 3 years ago 
[576] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 32: (= (+ b (* b)) 0) true
sat
(error "line 5 column 10: an invalid model was generated")
[577] % 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()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[578] % 
[578] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(assert (not (= (+ b (* 0 0 (* a 1))) (+ b (* b)) 0)))
(assert (>= b 0))
(check-sat)
[579] %
zhendongsu commented 3 years ago 
[587] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 27: (= (/ a (to_real 0)) b) false
25: (/ a (to_real 0))
0.0
26: b
(- 1.0)
sat
(error "line 5 column 10: an invalid model was generated")
[588] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
true l_false 50: (>= (/ a (to_real 0)) 0.0)
10 l_false l_false 50: (>= (/ a (to_real 0)) 0.0)
0  <= v5
updates 86
newlits 1 qhead: 1
neweqs  8 qhead: 8
(declare-fun / (Real Real) Real): b 25 
(declare-fun * (Real Real) Real): bc 45 40 
(declare-fun /0 (Real Real) Real): b 39 
(declare-fun to_real (Int) Real): un 24 
(declare-fun = (Real Real) Bool): bc 
#22 := a [p 25 39 44 45 43 53] [t 5:8] 
#37 := 1 [t 5:0] 
#38 := 1.0 [t 5:1] 
#23 := 0 [p 24] [t 5:2] 
#28 := 0.0 [p 42 25 39 42 40 47 48 43 44 48 53] [t 5:3] 
#24 := (to_real 0) [r 28] [p 25 39 42 40] [t 5:4] [j 28 --> 28 == 24] 
#25 := (/ a #24) [r 39] [p 41 40 27] [t 5:5] [j 39 sat: 1] 
#39 := (/0 a #24) [p 41 41 40 27 27 47] [t 5:6] 
#41 := (= #25 #39) [v1 := T] 
#42 := (= #24 0.0) [v2 := T] 
#40 := (* #24 #25) [r 28] [p 44 48 53] [t 5:7] [j 28 sat: 7] 
#44 := (= #40 a) [v3 := F] 
#26 := b [r 39] [p 27] [t 5:9] [j 25 sat: 4] 
#27 := (= #25 b) [v4 := T] 
#32 := (< #24 a) [v5 := T] [t 5:11] 
#30 := -1.0 [p 45] 
#45 := (* -1.0 a) [t 5:10] 
#47 := (= #25 0.0) [v6 := F] 
#48 := (= #40 0.0) [v7 := T] 
#43 := (= 0.0 a) [v8 := F] 
#49 := (<= #25 0.0) [v9 := T] [t 5:12] 
#50 := (>= #25 0.0) [v10 := F] [t 5:13] 
#51 := (>= #24 0.0) [v11 := T] [t 5:14] 
#52 := (<= #40 0.0) [v12 := T] [t 5:15] 
#53 := (= a #40) [v13 := F] 
bool-vars
1: 41 l_true (= #25 #39)
2: 42 l_true (= #24 0.0)
3: 44 l_false (= #40 a)
4: 27 l_true (= #25 b)
5: 32 l_true (< #24 a)
6: 47 l_false (= #25 0.0)
7: 48 l_true (= #40 0.0)
8: 43 l_false (= 0.0 a)
9: 49 l_true (<= #25 0.0)
10: 50 l_false (>= #25 0.0)
11: 51 l_true (>= #24 0.0)
12: 52 l_true (<= #40 0.0)
13: 53 l_false (= a #40)
number of constraints = 26
(0) j0 >= 1
(1) j0 <= 1
(2) j1 >= 1
(3) j1 <= 1
(4) j2 >= 0
(5) j2 <= 0
(6) j3 >= 0
(7) j3 <= 0
(8)  - j2 + j4 >= 0
(9)  - j2 + j4 <= 0
(11)  - j9 < 0
(12) j6 - j7 >= 0
(13) j6 - j7 <= 0
(14)  - j10 + j6 >= 0
(15)  - j10 + j6 <= 0
(16) j7 <= 0
(19) j7 < 0
(20) j4 >= 0
(22) j8 <= 0
(24)  - j8 + j3 >= 0
(25)  - j8 + j3 <= 0
 - j2 + j4
 - j9
j6 - j7
 - j10 + j6
 - j8 + j3
 -  j4 = 0
 +  j9 +  t11 = 0
 +  j6 -  j7 = 0
 -  j7 +  j10 = 0
 +  j8 = 0
----------------------
costs = 0
x*  1    1    0    0    0    0    -1    -1    0    1    -1    -1    0    0    0   
heading  -1    -2    -3    -4    -5    0    2    -7    -8    1    3    -9    -6    -10    4   
low  1    1    0    0    0    0                            0    0    0   
upp  1    1    0    0        0        -0.001    0            -0.001    0    0    0   

[0]    := (1, 0)               [(1, 0), (1, 0)]
[1]    := (1, 0)               [(1, 0), (1, 0)]
[2]    := (0, 0)               [(0, 0), (0, 0)]
[3]    := (0, 0)               [(0, 0), (0, 0)]
[4]    := (0, 0)               [(0, 0), oo]
[5]    := (0, 0) base          [(0, 0), (0, 0)]
- j2 + j4
[6]    := (-1, 0) base         [-oo, oo]
[7]    := (-1, 0)              [-oo, (0, -1)]
[8]    := (0, 0)               [-oo, (0, 0)]
[9]    := (1, 0) base          [-oo, oo]
[10]    := (-1, 0) base         [-oo, oo]
[11]    := (-1, 0)              [-oo, (0, -1)]
- j9
[12]    := (0, 0)               [(0, 0), (0, 0)]
j6 - j7
[13]    := (0, 0)               [(0, 0), (0, 0)]
- j10 + j6
[14]    := (0, 0) base          [(0, 0), (0, 0)]
- j8 + j3
[(j8 = 0 = (j4 = 0)*(j7 = -1))
[8]    := (0, 0)               [-oo, (0, 0)]
root=j8
]
vars:(j4 = 0)*(j7 = -1)
[4]    := (0, 0)               [(0, 0), oo]
root=j4
[7]    := (-1, 0)              [-oo, (0, -1)]
root=j7

same rvars, and m.rsign = 0 of course
v0 j0 = 1, int := 1
v1 j1 = 1 := 1.0
v2 j2 = 0, int := 0
v3 j3 = 0, shared := 0.0
v4 j4 = 0, shared := (to_real 0)
v5 j7 = -1 := (/ a (to_real 0))
v6 j6 = -1 := (/0 a (to_real 0))
v7 j8 = 0, shared := (* (to_real 0) (/ a (to_real 0)))
v8 j9 = 1, shared := a
v9 j10 = -1 := b
v10 t11 = -1 := (* -1.0 a)
v11 -5 l_false := (< (to_real 0) a)
v12 9 l_true := (<= (/ a (to_real 0)) 0.0)
v13 10 l_false := (>= (/ a (to_real 0)) 0.0)
v14 11 l_true := (>= (to_real 0) 0.0)
v15 12 l_true := (<= (* (to_real 0) (/ a #24)) 0.0)
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 582
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[589] % 
[589] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= (/ a 0) b))
(assert (< 0 a))
(check-sat)
[590] %
zhendongsu commented 3 years ago 
[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[512] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[513] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==23820==ERROR: AddressSanitizer: SEGV on unknown address 0x00000000000e (pc 0x56014e0121ee bp 0x7ffc63ebab70 sp 0x7ffc63eba970 T0)
==23820==The signal is caused by a READ memory access.
==23820==Hint: address points to the zero page.
    #0 0x56014e0121ed in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::move_table(obj_map<euf::enode, euf::enode*>::obj_map_entry*, unsigned int, obj_map<euf::enode, euf::enode*>::obj_map_entry*, unsigned int) ../src/util/hashtable.h:200
    #1 0x56014e0121ed in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::expand_table() ../src/util/hashtable.h:226
    #2 0x56014e0121ed in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::insert(obj_map<euf::enode, euf::enode*>::key_data&&) ../src/util/hashtable.h:393
    #3 0x56014e0121ed in obj_map<euf::enode, euf::enode*>::insert(euf::enode*, euf::enode* const&) ../src/util/obj_hashtable.h:141
    #4 0x56014e0121ed in dt::solver::occurs_check_enter(euf::enode*) ../src/sat/smt/dt_solver.cpp:589
    #5 0x56014e013477 in dt::solver::occurs_check(euf::enode*) ../src/sat/smt/dt_solver.cpp:637
    #6 0x56014e01455c in dt::solver::check() ../src/sat/smt/dt_solver.cpp:667
    #7 0x56014de546ca in euf::solver::check() ../src/sat/smt/euf_solver.cpp:457
    #8 0x56014fbfd2dc in sat::solver::final_check() ../src/sat/sat_solver.cpp:1752
    #9 0x56014fc24ecf in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1727
    #10 0x56014fc25d01 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1714
    #11 0x56014fc26e1f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1341
    #12 0x56014de43a62 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:66
    #13 0x56014de471c5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #14 0x56014ed3b3e8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #15 0x56014ed05fce in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #16 0x56014ed07977 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 0x56014eb5c730 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #18 0x56014eb7fd2f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #19 0x56014eb98774 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #20 0x56014eb6d6e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #21 0x56014eaef7d5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1623
    #22 0x56014ea46823 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2605
    #23 0x56014ea46823 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2947
    #24 0x56014ea46823 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #25 0x56014e9fbf55 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #26 0x56014bd8b96f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #27 0x56014bd36357 in main ../src/shell/main.cpp:372
    #28 0x7f1fa36efb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #29 0x56014bd4c109 in _start (/local/suz-local/software/z3san/build-04272021214656-30e904b/z3+0x206109)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/util/hashtable.h:200 in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::move_table(obj_map<euf::enode, euf::enode*>::obj_map_entry*, unsigned int, obj_map<euf::enode, euf::enode*>::obj_map_entry*, unsigned int)
==23820==ABORTING
[514] % 
[514] % cat small.smt2
(declare-datatypes ((nat 0) (list 0) (a 0)) (((b (c nat)) (d)) ((cons (car a) (cdr list)) (m)) ((n (children list)) (e (data nat)))))
(declare-fun f () nat)
(declare-fun g () list)
(declare-fun h () list)
(declare-fun i () list)
(declare-fun j () a)
(declare-fun k () a)
(declare-fun l () a)
(declare-fun o () nat)
(declare-fun p () a)
(declare-fun q () nat)
(declare-fun r () a)
(assert (and (or (or false (and (not (distinct (n h) k)) (= g (cons r i))(distinct f (b o))) ((_ is e) j)) ((_ is b) q)) (distinct p l)))
(check-sat)
[515] %
zhendongsu commented 3 years ago

This one seems tough to reduce:

[650] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 50: (= q (bvor (bvor #41) (bvshl #46 bv[24:32]))) false
31: q
#xff0000ff
49: (bvor (bvor (bvor #37 #39 bv[16:32])) (bvshl (concat bv[0:24] #45) bv[24:32]))
#xff000010
Failed to validate 52: (= l (if (= q #49) bv[1:1] bv[0:1])) false
30: l
#b1
51: (if (= q (bvor #42 #48)) bv[1:1] bv[0:1])
#b0
Failed to validate 10891: (= bv[1:1] (bvnand (if #28 bv[1:1] bv[0:1]) (bvand #174 #176))) true
sat
(error "line 56 column 10: an invalid model was generated")
[651] % 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()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[652] % 
[652] % cat small.smt2
(declare-fun ag () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 1))
(declare-fun af () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(declare-fun d () (_ BitVec 1))
(declare-fun g () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(declare-fun f () (_ BitVec 1))
(declare-fun k () (_ BitVec 1))
(declare-fun l () (_ BitVec 1))
(declare-fun h () (_ BitVec 1))
(declare-fun i () (_ BitVec 32))
(declare-fun ab () (_ BitVec 32))
(declare-fun j () (_ BitVec 32))
(declare-fun q () (_ BitVec 32))
(declare-fun r () (_ BitVec 32))
(declare-fun m () (_ BitVec 32))
(declare-fun n () (_ BitVec 1))
(declare-fun o () (_ BitVec 32))
(declare-fun p () (_ BitVec 1))
(declare-fun u () (_ BitVec 32))
(declare-fun v () (_ BitVec 32))
(declare-fun s () (_ BitVec 32))
(declare-fun ac () (_ BitVec 32))
(declare-fun t () (_ BitVec 32))
(declare-fun ad () (_ BitVec 32))
(assert (distinct (_ bv1 1) (bvnand (ite (= h (ite (= m j) (_ bv1 1)
   (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (bvand (ite (= l (ite (= q
   (bvor (bvor (bvor (concat (_ bv0 24) (select a (bvadd r))) (concat
   (_ bv0 24) (select a r)) (_ bv16 32))) (bvshl (concat (_ bv0 24)
   (select a (bvsmod r (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0
   1))) (ite (= k (ite (= r (bvadd s)) (_ bv1 1) (_ bv0 1))) (ite (= f
   n) (_ bv1 1) (_ bv0 1)) (bvand (bvand (bvand (ite (= e (ite (= i
   (bvor (bvashr (bvor (concat (_ bv0 24) (select a (bvadd ab (_ bv0
   32)))) (bvshl (concat (_ bv0 24) (select a (bvadd ab (_ bv1 32))))
   (_ bv8 32))) (bvshl (concat (_ bv0 24) (select a (bvshl ab (_ bv2
   32)))) (_ bv16 32))))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))
   (bvand (ite (= g (ite (= ab (bvadd s)) (_ bv1 1) (_ bv0 1))) (_ bv1
   1) (bvadd (bvsdiv (ite distinct (_ bv1 1) (_ bv0 1)) (bvmul (ite (=
   d (ite (= o (concat (_ bv0 31) p)) (_ bv1 1) (_ bv0 1))) (_ bv1 1)
   (bvudiv (ite (= c (ite (= u (bvor (bvor (bvor (concat (_ bv0 24)
   (select a (bvsdiv v (_ bv0 32))))) (bvshl (concat (_ bv0 24)
   (select a v)) (_ bv16 32))))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_
   bv0 1)) (bvand (ite (= af (ite (= v (bvsmod s (_ bv8 32))) (_ bv1
   1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= b (ite (= a
   (store (store (store (store ag (bvadd s (_ bv3 32)) ((_ extract 7
   0) (bvxor t))) (bvadd s) ((_ extract 7 0) (bvlshr t (_ bv16 32))))
   (bvadd s) ((_ extract 7 0) (bvlshr t (_ bv8 32)))) s ((_ extract 7
   0) t))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (=
   (ite (distinct s) (_ bv1 1) (_ bv0 1))(ite (= ac (bvurem (bvor
   (bvshl (concat ad) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select
   ag (bvadd (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1
   1) (_ bv0 1)))))))))))))))) b)) (ite (= ac m) (_ bv1 1) (_ bv0
   1))))))
(check-sat)
[653] %
zhendongsu commented 3 years ago 
[535] % z3release small.smt2
sat
[536] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[537] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 2360
ax_is_correct()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[538] % 
[538] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e (Int) Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h (Int) Int)
(assert (not (=> (= f g 5) (= a (- f)) (>= b (- f g)) (= b (- (+ a (* 2 c)) (* 2 (e c))) (h b)) (= (h (+ b 1)) d))))
(check-sat)
[539] %
zhendongsu commented 3 years ago 
[548] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 47: (= (j e) (car k)) false
33: (j e)
(j d)
46: (car k)
(i h)
sat
(error "line 9 column 10: an invalid model was generated")
[549] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 47: (= (j e) (car k)) false
33: (j e)
(j d)
46: (car k)
(i h)
sat
(error "line 9 column 10: an invalid model was generated")
[550] % 
[550] % cat small.smt2
(declare-datatypes ((a 0)(b 0)(c 0)) (((d)) ((cons (car c) (cdr b)) (h)) ((i (children b)) (j (data a)))))
(declare-fun e () a)
(declare-fun f () a)
(declare-fun k () b)
(declare-fun g () b)
(declare-fun l () c)
(assert (or (and (distinct k (children (i (cons (car g) k)))) ((_ is d) f)) (not (distinct (i (children (j e))) l))))
(assert (= (j e) (car k)))
(check-sat)
[551] %
zhendongsu commented 3 years ago 
[557] % 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: 121
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[558] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(assert
 (=
  (= (_ bv0 32)
   ((_ zero_extend 16)
    (concat
     (select a
      ((_ extract 31 0)
       ((_ zero_extend 56)
        ((_ extract 7 0)
         ((_ zero_extend 4)
          (select b (_ bv7 32)))))))
     (select a
      ((_ extract 31 0)
       ((_ zero_extend 56)
        ((_ extract 7 0)
         ((_ zero_extend 4)
          (select b (_ bv7 32))))))))))
  false))
(check-sat)
[559] %
zhendongsu commented 3 years ago 
[568] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 72: (= (bvor (bvor #58)) (bvor (bvor #65 #69))) true
Failed to validate 75: (= bv[1:1] (if (not #72) bv[1:1] bv[0:1])) false
49: bv[1:1]
#b1
74: (if (not (= #60 #71)) bv[1:1] bv[0:1])
#b0
sat
(error "line 18 column 10: an invalid model was generated")
[569] % 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()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[570] % 
[570] % cat small.smt2
(declare-fun mem_35_93 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EBP_0_60 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert
(let ((?b (store (store (store (store mem_35_93 (bvadd (bvsub
          R_ESP_1_58 (_ bv4 32)) (_ bv3 32)) ((_ extract 7 0) (bvlshr
          R_EBP_0_60 (_ bv24 32)))) (bvadd (_ bv2 32)) ((_ extract 7
          0) (bvlshr R_EBP_0_60 (_ bv16 32)))) (bvadd (_ bv1 32)) ((_
          extract 7 0) (bvlshr R_EBP_0_60 (_ bv8 32)))) (bvadd (bvsub
          R_ESP_1_58 (_ bv4 32))) ((_ extract 7 0) R_EBP_0_60)))
      (?c (bvadd (bvsub R_ESP_1_58 (_ bv4 32)) (_ bv4 32))))
   (= (_ bv1 1) (ite (not (= (bvor (bvor (bvor (bvshl (concat (_ bv0
   24) (select mem_35_93 (bvadd R_ESP_1_58 (_ bv1 32)))) (_ bv8
   32))(concat (_ bv0 24) (select mem_35_93 (bvadd R_ESP_1_58 (_ bv2
   32))))))) (bvor (bvor (bvor (bvshl (concat (_ bv0 24) (?b (bvadd ?c
   (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (?b (bvadd ?c
   (_ bv2 32)))) (_ bv16 32)))))) (_ bv1 1) (_ bv0 1)))))
(check-sat)
[571] %
NikolajBjorner commented 3 years ago

Thanks for targeting the new code. It is a very good use of the fuzzing facilities and helps reaching a more solid state for this so-far not exercised code. All bugs reported in this thread have now been fixed.