From bd48b76f2f4fac6ea6f70db8c0300c4ad589e8e6 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Wed, 25 May 2022 12:12:15 +0200 Subject: [PATCH 1/2] handle undefined results from model evaluation --- .../apalache/tla/bmcmt/smt/Z3SolverContext.scala | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 61271f8d8f..2e8194cf3f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -331,8 +331,16 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { val (smtEx, _) = toExpr(ex) val z3expr = z3solver.getModel.eval(smtEx, true) if (z3expr.isBool) { - val isTrue = z3expr.getBoolValue.equals(Z3_lbool.Z3_L_TRUE) - ValEx(if (isTrue) TlaBool(true) else TlaBool(false)) // in undefined case, just return false + z3expr.getBoolValue match { + case Z3_lbool.Z3_L_TRUE => + ValEx(TlaBool(true)) + case Z3_lbool.Z3_L_FALSE => + ValEx(TlaBool(false)) + case _ => + // If we cannot get a result from evaluating the model, we query the solver + z3solver.add(z3expr.asInstanceOf[BoolExpr]) + ValEx(TlaBool(sat())) + } } else if (z3expr.isIntNum) { ValEx(TlaInt(z3expr.asInstanceOf[IntNum].getBigInteger)) } else { From 38531dc207fe5a688955e1440ccd4682b1e1ebf5 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Wed, 25 May 2022 13:33:34 +0200 Subject: [PATCH 2/2] update release notes --- .unreleased/bug-fixes/1819.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/1819.md diff --git a/.unreleased/bug-fixes/1819.md b/.unreleased/bug-fixes/1819.md new file mode 100644 index 0000000000..2934a56756 --- /dev/null +++ b/.unreleased/bug-fixes/1819.md @@ -0,0 +1 @@ +Fix nested set membership in the arrays encoding, see #1819 \ No newline at end of file