Work around Z3 not producing models for some quantified expressions

Z3's solve_eqs preprocessor eliminates a Boolean symbol defined via
(assert (= symbol <quantified-expr>)) by substituting the quantified
expression, and then returns that quantified expression from get-value
instead of a Boolean value, which CBMC cannot parse (see
Z3Prover/z3#7743).

Emit the equivalence as two implications, (=> symbol <expr>) and
(=> <expr> symbol), which solve_eqs does not treat as an elimination
opportunity, while preserving logical equivalence. A let-binding shares
the quantified expression so that it is emitted only once. As this is a
Z3-specific problem, the workaround is gated on the Z3 solver; other
solvers keep the single equality assertion. Z3 >= 4.15.3 offers the
opt-in option smt.solve_eqs.non_ground (default: true), which avoids
this elimination when set to false, but Z3's default behaviour is
unchanged and older versions reject the option.

This reinstates
regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check
as CORE: it was demoted to KNOWNBUG in b0eedde precisely because of
this Z3 misbehaviour. Likewise, regression/cbmc/z3/Issue5977.desc again
expects exactly "unknown", and Quantifiers-assertion,
Quantifiers-initialisation2, and Quantifiers-two-dimension-array now
pass with Z3 and are no longer tagged broken-z3-smt-backend. A unit test
in unit/solvers/smt2/smt2_conv.cpp additionally pins the exact SMT2
output for both Z3 and other solvers.

Quantifiers that reach Z3 via other definitions, such as an assignment
to a non-Boolean symbol, are handled in the next commit.

Runtime of `cbmc --z3` (Z3 4.8.12) is unchanged on the quantifier tests
that already passed before. Tests that previously stopped with an error
right after the first solver call now run to completion, e.g.,
Quantifiers-initialisation2 takes 11.9s (previously an error after
1.4s).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -1,4 +1,4 @@
-KNOWNBUG smt-backend no-new-smt
+CORE smt-backend no-new-smt
 smt_missing_range_check.c
 --no-malloc-may-fail --pointer-check -z3
 ^EXIT=10$
@@ -13,6 +13,3 @@ quantifier, for out of bounds memory access, when using the smt backend and
 the range of the index is unbound. Note that this test is not expected to work
 with the SAT backend at the time of writing, as the SAT backend does not support
 quantifiers in this form.
-
-Neither Z3 nor CVC5 currently return complete models, and Bitwuzla does not
-complete in more than 5 minutes.

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend no-new-smt
+CORE no-new-smt
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend no-new-smt
+CORE no-new-smt
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -1,4 +1,4 @@
-CORE broken-z3-smt-backend no-new-smt
+CORE no-new-smt
 main.c
 
 ^\*\* Results:$

regression/cbmc/z3/Issue5977.desc

@@ -1,9 +1,9 @@
 CORE smt-backend broken-cprover-smt-backend no-new-smt
 Issue5977.c
 --z3
-^EXIT=(6|10)$
+^EXIT=6$
 ^SIGNAL=0$
-^SMT2 solver returned ("unknown"|non-constant value for variable B\d+)$
+^SMT2 solver returned "unknown"$
 --
 --
 This tests that an "unknown" result from the SMT solver is reported.

src/solvers/smt2/smt2_conv.cpp

@@ -985,17 +985,42 @@ literalt smt2_convt::convert(const exprt &expr)
   // Note that here we are always converting, so we do not need to consider
   // other literal kinds, only "|B###|"
 
-  // Z3 refuses get-value when a defined symbol contains a quantifier.
+  // Z3 refuses get-value when a defined symbol contains a quantifier, so we
+  // declare the symbol and constrain it separately rather than using
+  // define-fun.
   if(has_quantifier(prepared_expr))
   {
     out << "(declare-fun ";
     convert_literal(l);
     out << " () Bool)\n";
-    out << "(assert (= ";
-    convert_literal(l);
-    out << ' ';
-    convert_expr(prepared_expr);
-    out << "))\n";
+    if(solver == solvert::Z3)
+    {
+      // A single (assert (= B <expr>)) does not help on Z3: its solve_eqs
+      // preprocessor eliminates B by substituting the quantified <expr>, and
+      // then hands the eliminated form back through get-value (see
+      // Z3Prover/z3#7743). Asserting the equivalence as two implications
+      // instead prevents this; a let-binding shares the (possibly large)
+      // quantified expression so that it is emitted only once. Z3 >= 4.15.3
+      // offers the opt-in option smt.solve_eqs.non_ground (default: true),
+      // which avoids this elimination when set to false, but Z3's default
+      // behaviour is unchanged and older versions reject the option, so we
+      // keep this encoding for Z3.
+      out << "(assert (let ((?def ";
+      convert_expr(prepared_expr);
+      out << ")) (and (=> ";
+      convert_literal(l);
+      out << " ?def) (=> ?def ";
+      convert_literal(l);
+      out << "))))\n";
+    }
+    else
+    {
+      out << "(assert (= ";
+      convert_literal(l);
+      out << ' ';
+      convert_expr(prepared_expr);
+      out << "))\n";
+    }
   }
   else
   {

unit/solvers/smt2/smt2_conv.cpp

@@ -869,3 +869,68 @@ TEST_CASE(
     REQUIRE(smt2_dec() == decision_proceduret::resultt::D_UNSATISFIABLE);
   }
 }
+
+/// Helper: full SMT2 emitted by converting (handling) a Boolean expression
+static std::string convert_handle(const exprt &expr, smt2_convt::solvert solver)
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  std::ostringstream out;
+  smt2_convt conv(ns, "test", "", "QF_BV", solver, out);
+  conv.handle(expr);
+  return out.str();
+}
+
+TEST_CASE("smt2_convt quantifier definition encoding", "[core][solvers][smt2]")
+{
+  // A Boolean handle whose definition contains a quantifier cannot be emitted
+  // as a `define-fun` (Z3 rejects `get-value` on such a symbol), so it is
+  // declared and constrained separately.
+  const unsignedbv_typet bv8{8};
+  const symbol_exprt i{"i", bv8};
+  const exists_exprt quantified{i, equal_exprt{i, from_integer(0, bv8)}};
+  const std::string quant = "(exists ((i (_ BitVec 8))) (= i (_ bv0 8)))";
+
+  GIVEN("a quantified Boolean expression and the Z3 solver")
+  {
+    const std::string out = convert_handle(quantified, smt2_convt::solvert::Z3);
+    INFO("SMT2 output:\n" << out);
+
+    THEN("it is declared and constrained by a let-bound equivalence")
+    {
+      // A single `(assert (= B0 <quantifier>))` would be undone by Z3's
+      // solve_eqs preprocessor (Z3Prover/z3#7743), so the equivalence is
+      // emitted as two implications. A let-binding shares the quantified
+      // expression so that it is written only once.
+      const std::string declare = "(declare-fun B0 () Bool)";
+      const std::string assertion =
+        "(assert (let ((?def " + quant + ")) (and (=> B0 ?def) (=> ?def B0))))";
+
+      REQUIRE(out.find(declare) != std::string::npos);
+      REQUIRE(out.find(assertion) != std::string::npos);
+      // the quantified expression is emitted exactly once
+      REQUIRE(out.find(quant) == out.rfind(quant));
+      // no plain equality definition
+      REQUIRE(out.find("(assert (= B0 ") == std::string::npos);
+    }
+  }
+
+  GIVEN("a quantified Boolean expression and a generic solver")
+  {
+    const std::string out =
+      convert_handle(quantified, smt2_convt::solvert::GENERIC);
+    INFO("SMT2 output:\n" << out);
+
+    THEN("it is declared and constrained by a single equality")
+    {
+      // The Z3-specific solve_eqs workaround is not applied to other solvers.
+      const std::string declare = "(declare-fun B0 () Bool)";
+      const std::string equality = "(assert (= B0 " + quant + "))";
+
+      REQUIRE(out.find(declare) != std::string::npos);
+      REQUIRE(out.find(equality) != std::string::npos);
+      // no implication-based workaround
+      REQUIRE(out.find("(assert (=> ") == std::string::npos);
+    }
+  }
+}