From 57086edc42e1be63b5c0db3837ddd2e3b1ba17e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Jun 2020 03:06:58 -0700 Subject: [PATCH] close #4432 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 3 +++ src/qe/qsat.cpp | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index ec3a7d09f..4d46929a9 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -345,6 +345,9 @@ namespace qe { if (is_arith(v) && !tids.contains(v)) { rational r; expr_ref val = eval(v); + if (!m.inc()) + return vector(); + VERIFY(a.is_numeral(val, r)); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); tids.insert(v, mbo.add_var(r, a.is_int(v))); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 8f78a9106..4f903e815 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -647,8 +647,10 @@ namespace qe { switch (res) { case l_true: s.get_model(m_model); + if (!m_model) + return l_undef; SASSERT(validate_defs("check_sat")); - SASSERT(validate_assumptions(*m_model.get(), asms)); + SASSERT(!m_model.get() || validate_assumptions(*m_model.get(), asms)); SASSERT(validate_model(asms)); TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); if (m_level == 0) {