mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Fix for previous commit.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-19 12:07:33 +01:00
parent 11997afb5d
commit 948bf9540f
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_arith_nl.h
View file

@ -590,7 +590,7 @@ namespace smt {
bool propagated = false;
context & ctx = get_context();
for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
theory_var v = m_nl_monomials.size();
theory_var v = m_nl_monomials[i];
expr * m = var2expr(v);
if (!ctx.is_relevant(m))
continue;
@ -705,7 +705,7 @@ namespace smt {
unsigned n = 0;
numeral range;
for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
theory_var v = m_nl_monomials.size();
theory_var v = m_nl_monomials[i];
if (is_real(v))
continue;
bool computed_epsilon = false;
@ -2337,7 +2337,7 @@ namespace smt {
var_set already_found;
svector<theory_var> vars;
for (unsigned i = 0; i < m_nl_monomials.size(); i++) {
theory_var v = m_nl_monomials.size();
theory_var v = m_nl_monomials[i];
mark_var(v, vars, already_found);
expr * n = var2expr(v);
SASSERT(is_pure_monomial(n));