From 260f759177926056c1b460a92ed93f46bd041c9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Nov 2020 20:06:32 -0800 Subject: [PATCH] fix #4835 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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)