Skip to content
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

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

Closed
zhendongsu opened this issue Apr 28, 2021 · 17 comments
Closed

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

zhendongsu opened this issue Apr 28, 2021 · 17 comments

Comments

@zhendongsu
Copy link

Commit: 30e904b

[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
Copy link
Author

zhendongsu commented Apr 28, 2021 •
edited
Loading 

[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 zhendongsu changed the title [Consolidated] soundness issues and crashes for options "tactic.default_tactic=smt sat.euf=true" [Consolidated] soundness issues, invalid models, and crashes for options "tactic.default_tactic=smt sat.euf=true" Apr 28, 2021
@zhendongsu
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author

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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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 added a commit that referenced this issue May 1, 2021
@NikolajBjorner
#5223
6de0615
NikolajBjorner added a commit that referenced this issue May 1, 2021
@NikolajBjorner
#5223
7835388
NikolajBjorner added a commit that referenced this issue May 1, 2021
@NikolajBjorner
#5223
323e0e6
NikolajBjorner added a commit that referenced this issue May 2, 2021
@NikolajBjorner
#5223
0810720
NikolajBjorner added a commit that referenced this issue May 2, 2021
@NikolajBjorner
#5223
51a4db8
NikolajBjorner added a commit that referenced this issue May 5, 2021
@NikolajBjorner
#5223
85bd4b5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner added a commit that referenced this issue May 5, 2021
@NikolajBjorner
#5223
87c0a81
NikolajBjorner added a commit that referenced this issue May 5, 2021
@NikolajBjorner
#5223
7e330c1
NikolajBjorner added a commit that referenced this issue May 6, 2021
@NikolajBjorner
#5223
7e7360d
NikolajBjorner added a commit that referenced this issue May 29, 2021
@NikolajBjorner
#5223
4d41db2 
unreachable code in dual solver
NikolajBjorner added a commit that referenced this issue May 31, 2021
@NikolajBjorner
#5223
fb75dac
NikolajBjorner added a commit that referenced this issue May 31, 2021
@NikolajBjorner
#5223
fe0727d
NikolajBjorner added a commit that referenced this issue May 31, 2021
@NikolajBjorner
#5223
8d1dfb9
@NikolajBjorner
Copy link
Contributor

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.

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
2 participants
@NikolajBjorner @zhendongsu