mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix #4437, not really interesting bug as debug assertion is really for non-interrupted flow
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
df75792e9c
commit
04829e6b7a
|
@ -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()));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -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 =
|
||||
|
|
Loading…
Reference in a new issue