From 04829e6b7a75199f33d0c832f9543b6c11b07dc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:41:26 -0700 Subject: [PATCH] fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 2 +- src/qe/qsat.cpp | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3de37129e..31c9771b1 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2054,7 +2054,7 @@ public class Context implements AutoCloseable { public SeqExpr MkNth(SeqExpr s, Expr index) { checkContextMatch(s, index); - return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 248344c21..8f78a9106 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -166,7 +166,9 @@ namespace qe { expr_ref val(m); for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { app* p = m_preds[level - 1][j].get(); - eval(p, val); + eval(p, val); + if (!m.inc()) + return; if (m.is_false(val)) { m_asms.push_back(m.mk_not(p)); } @@ -179,6 +181,8 @@ namespace qe { for (unsigned i = level + 1; i < m_preds.size(); i += 2) { for (unsigned j = 0; j < m_preds[i].size(); ++j) { + if (!m.inc()) + return; app* p = m_preds[i][j].get(); max_level lvl = m_elevel.find(p); bool use =