mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #4131

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 13:07:25 -07:00
parent e3f712b3cf
commit 1f9e022168
2 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/diff_logic.h
View file

@ -264,13 +264,11 @@ class dl_graph {
public: public:
// An assignment is feasible if all edges are feasible. // An assignment is feasible if all edges are feasible.
bool is_feasible() const { bool is_feasible() const {
#ifdef Z3DEBUG
for (unsigned i = 0; i < m_edges.size(); ++i) { for (unsigned i = 0; i < m_edges.size(); ++i) {
if (!is_feasible(m_edges[i])) { if (!is_feasible(m_edges[i])) {
return false; return false;
} }
} }
#endif
return true; return true;
} }

5
src/smt/theory_diff_logic_def.h
View file

@ -341,9 +341,8 @@ void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);
unsigned num_edges = m_graph.get_num_edges(); unsigned num_edges = m_graph.get_num_edges();
m_graph.pop(num_scopes); m_graph.pop(num_scopes);
TRACE("arith", m_graph.display(tout);); CTRACE("arith", !m_graph.is_feasible(), m_graph.display(tout););
SASSERT(m_graph.is_feasible()); if (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0) {
if (true || (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0)) {
m_S.reset(); m_S.reset();
m_num_simplex_edges = 0; m_num_simplex_edges = 0;
m_objective_rows.reset(); m_objective_rows.reset();