From a94e2e62af13cb23c14e97f7d4441327550040db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Oct 2021 11:28:09 +0200 Subject: [PATCH] build warnings --- src/sat/smt/arith_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 89b778672fa..76f1d9a0a55 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -627,7 +627,7 @@ namespace arith { anum const& an = nl_value(v, *m_a1); if (a.is_int(o) && !m_nla->am().is_int(an)) value = a.mk_numeral(rational::zero(), a.is_int(o)); - value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); + //value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); } else if (v != euf::null_theory_var) { rational r = get_value(v);