From a74c01c8b98088ed096e7c046a8baa1906cf5f24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 20:39:54 -0700 Subject: [PATCH] #5528 --- src/sat/smt/arith_internalize.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index e59d3f4d7..d8671c910 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -42,6 +42,7 @@ namespace arith { void solver::init_internalize() { force_push(); // initialize 0, 1 variables: + if (!m_internalize_initialized) { get_one(true); get_one(false); @@ -484,10 +485,10 @@ namespace arith { 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);