From 968717a532baaa6b5bdf56a688a6380bc7791a0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:49:39 -0700 Subject: [PATCH] follow on fix from #5528 the same bug is also undetected in the main solver --- src/smt/theory_lra.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index abe10d0f3..124461189 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -807,10 +807,10 @@ class theory_lra::imp { return st.vars()[0]; } else if (is_one(st) && a.is_numeral(term)) { - return get_one(a.is_int(term)); + return lp().local_to_external(get_one(a.is_int(term))); } else if (is_zero(st) && a.is_numeral(term)) { - return get_zero(a.is_int(term)); + return lp().local_to_external(get_zero(a.is_int(term))); } else { init_left_side(st);