From 0f83e7a251a4d1f094d3abba2c76e6c7512e032f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 12:23:34 -0700 Subject: [PATCH] fix bug masked by default configuration Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index bce59657a..d08e6f13a 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -118,7 +118,7 @@ public: void mk_eq(expr * arg1, expr * arg2, expr_ref & result) { if (mk_eq_core(arg1, arg2, result) == BR_FAILED) - result = m_util.mk_le(arg1, arg2); + result = m_util.mk_eq(arg1, arg2); } void mk_le(expr * arg1, expr * arg2, expr_ref & result) { if (mk_le_core(arg1, arg2, result) == BR_FAILED)