mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 20:50:50 +00:00
Code Activity

fix #3351

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-16 12:05:35 -07:00
parent bb1fe358c1
commit 3209d4ff6c
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_utvpi_def.h
View file

@ -377,7 +377,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool theory_utvpi<Ext>::internalize_term(app * term) { bool theory_utvpi<Ext>::internalize_term(app * term) {
bool result = null_theory_var != mk_term(term); bool result = !get_context().inconsistent() && null_theory_var != mk_term(term);
CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";); CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
return result; return result;
} }
@ -649,10 +649,10 @@ namespace smt {
if (terms.size() >= 2) { if (terms.size() >= 2) {
v2 = terms[1].first; v2 = terms[1].first;
pos2 = terms[1].second.is_one(); pos2 = terms[1].second.is_one();
SASSERT(v1 != null_theory_var); SASSERT(v2 != null_theory_var);
SASSERT(pos2 || terms[1].second.is_minus_one()); SASSERT(pos2 || terms[1].second.is_minus_one());
} }
// TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";); TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";);
edge_id id = m_graph.get_num_edges(); edge_id id = m_graph.get_num_edges();
th_var w1 = to_var(v1), w2 = to_var(v2); th_var w1 = to_var(v1), w2 = to_var(v2);