1

Closed

assertion violation: m_clauses.contains(&c)

description

Version:
End of master branch built with Z3DEBUG=1 and _EXTERNAL_RELEASE=1, plus cherry-picked changes:
https://z3.codeplex.com/SourceControl/changeset/110fa0b7fb711418fe2be67f033e8ed70b354972
https://z3.codeplex.com/SourceControl/changeset/f4f1c63abb4a6fd0df908e376b0ab014bce3d9da

Don't know if it has the same cause as issue 47.
ASSERTION VIOLATION
File: third-party/z3/src/sat/sat_clause_use_list.h
Line: 80
m_clauses.contains(&c)
#2  0x0000000000b2247e in sat::clause_use_list::erase (this=0x7ffff7fccdc0, c=...) at third-party/z3/src/sat/sat_clause_use_list.h:80
#3  0x0000000000b1d60e in sat::use_list::erase (this=0x7fffffffc7c8, c=...) at third-party/z3/src/sat/sat_simplifier.cpp:44
#4  0x0000000000b22bd6 in sat::simplifier::remove_clause (this=0x7fffffffc7b8, c=...) at third-party/z3/src/sat/sat_simplifier.cpp:107
#5  0x0000000000b1feb1 in sat::simplifier::subsume (this=0x7fffffffc7b8) at third-party/z3/src/sat/sat_simplifier.cpp:825
#6  0x0000000000b1dea3 in sat::simplifier::operator() (this=0x7fffffffc7b8, learned=false) at third-party/z3/src/sat/sat_simplifier.cpp:167
#7  0x0000000000b09f7c in sat::solver::simplify_problem (this=0x7fffffffc418) at third-party/z3/src/sat/sat_solver.cpp:865
#8  0x0000000000b0963f in sat::solver::check (this=0x7fffffffc418) at third-party/z3/src/sat/sat_solver.cpp:698
#9  0x0000000000a17091 in sat_tactic::imp::operator() (this=0x7fffffffc400, g=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/sat/tactic/sat_tactic.cpp:70
#10 0x0000000000a1787d in sat_tactic::operator() (this=0x13c4ab8, g=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/sat/tactic/sat_tactic.cpp:174
#11 0x0000000000bdacf6 in cleanup_tactical::operator() (this=0x13c4b08, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1206
#12 0x0000000000bdb371 in cond_tactical::operator() (this=0x13c62a8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1303
#13 0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13c9c88, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#14 0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13c9cc8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#15 0x0000000000bdb371 in cond_tactical::operator() (this=0x13cb4d8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1303
#16 0x0000000000bdb335 in cond_tactical::operator() (this=0x13cb558, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1301
#17 0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13cb5a8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#18 0x0000000000bd942a in unary_tactical::operator() (this=0x13cb5e8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:989
#19 0x0000000000be7864 in exec (t=..., in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactic.cpp:180
#20 0x0000000000be7ad8 in check_sat (t=..., g=..., md=..., pr=..., core=..., reason_unknown=...) at third-party/z3/src/tactic/tactic.cpp:202
Test case attached.

file attachments

Closed Jun 13, 2013 at 9:48 PM by leodemoura
Fixed in the unstable branch.

comments

leodemoura wrote Jun 13, 2013 at 9:47 PM