From 8de8c4cade20d4df070725b53646bf912820c702 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Aug 2018 11:41:06 -0700 Subject: [PATCH] fix #1798 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 54f61a09a..c11c54b69 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -504,9 +504,9 @@ namespace smt { tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); - mk_axiom(eqz, eq, !is_numeral); - mk_axiom(eqz, lower, !is_numeral); - mk_axiom(eqz, upper, !is_numeral); + mk_axiom(eqz, eq, true); + mk_axiom(eqz, lower, false); + mk_axiom(eqz, upper, false); rational k; context& ctx = get_context(); (void)ctx;