From 65e1d0845720763705af7465548b6b5aaa9887e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2020 10:23:31 -0700 Subject: [PATCH] disabling linearization when canceled, #3412 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index d46bdde5a..919a3c3af 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -67,6 +67,9 @@ namespace qe { CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";); SASSERT(m.canceled() || m.is_true(val));); + if (!m.inc()) + return false; + TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";); bool is_not = m.is_not(lit, lit); if (is_not) {