mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
fix crash reported in #784
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
865c0c0109
commit
e0613b6737
|
@ -141,6 +141,8 @@ namespace sat {
|
|||
CASSERT("sat_solver", s.check_invariant());
|
||||
TRACE("before_simplifier", s.display(tout););
|
||||
|
||||
m_sub_todo.reset();
|
||||
m_sub_bin_todo.reset();
|
||||
s.m_cleaner(true);
|
||||
m_last_sub_trail_sz = s.m_trail.size();
|
||||
TRACE("after_cleanup", s.display(tout););
|
||||
|
|
|
@ -3078,6 +3078,10 @@ namespace sat {
|
|||
m_binary_clause_graph[l1.index()].push_back(l2);
|
||||
m_binary_clause_graph[l2.index()].push_back(l1);
|
||||
}
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
m_binary_clause_graph.reserve(lits[i].index() + 1);
|
||||
m_binary_clause_graph.reserve((~lits[i]).index() + 1);
|
||||
}
|
||||
bool non_empty = true;
|
||||
m_seen[0].reset();
|
||||
while (non_empty) {
|
||||
|
|
Loading…
Reference in a new issue