diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1f74dd592..b4c76fc6e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -384,7 +384,7 @@ class theory_lra::imp { vars.push_back(v); ++index; } - else if(a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) { + else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) { theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned()); coeffs[vars.size()] = coeffs[index]; vars.push_back(v); @@ -510,6 +510,7 @@ class theory_lra::imp { theory_var v = mk_var(t); if (_has_var) return v; + VERIFY(internalize_term(n)); theory_var w = mk_var(n); svector vars; for (unsigned i = 0; i < p; ++i)