mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

finetune

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-01 15:40:02 -07:00
parent 8849cef4b7
commit 7343783efe
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -2424,11 +2424,13 @@ public:
} }
void add_eq(lpvar u, lpvar v, lp::explanation const& e) { void add_eq(lpvar u, lpvar v, lp::explanation const& e) {
if (ctx().inconsistent())
return;
theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
enode* n1 = get_enode(uv); enode* n1 = get_enode(uv);
enode* n2 = get_enode(vv); enode* n2 = get_enode(vv);
if (n1 == n2) if (n1->get_root() == n2->get_root())
return; return;
reset_evidence(); reset_evidence();
for (auto const& ev : e) for (auto const& ev : e)
@ -2442,7 +2444,6 @@ public:
ctx().assign_eq(n1, n2, eq_justification(js)); ctx().assign_eq(n1, n2, eq_justification(js));
} }
literal_vector m_core2; literal_vector m_core2;
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) { void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params) {