Define a Boolean variable per quantifier when using Z3

The previous commit makes Z3 return Boolean values for variables that
are defined via a quantified expression. Quantifiers may also be part
of other definitions, such as an assignment to a non-Boolean symbol (in
`int x = __CPROVER_forall { ... };`, x is defined via an if-then-else
over the quantifier), or of Boolean definitions that use define-fun.
Z3's solve_eqs preprocessor eliminates these symbols, too, and then
returns quantified expressions from get-value.

With Z3, now replace each quantifier that is not nested within another
quantifier by a fresh Boolean variable, defined using the encoding of
the previous commit, so that no other definition contains a quantifier.

Quantifiers-assignment, Quantifiers-if, and Quantifiers-not now pass
with Z3 and are no longer tagged broken-z3-smt-backend. Their runtime
with Z3 4.8.12 is 11.5s, 0.14s, and 0.14s, respectively (previously,
these stopped with an error after 5.3s, 0.09s, and 0.09s).
Quantifiers-not-exists/fixed.desc remains broken with Z3: it now
reports an error after 83s, previously after 0.09s.

Fixes: #8679

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

Author: tautschnig

regression/cbmc/Quantifiers-assignment/test.desc

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

regression/cbmc/Quantifiers-if/test.desc

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

regression/cbmc/Quantifiers-not/test.desc

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

src/solvers/smt2/smt2_conv.cpp

@@ -5725,10 +5725,29 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr)
     !has_byte_operator(lowered_expr),
     "lower_byte_operators should remove all byte operators");
 
+  // With Z3, quantifiers that are not nested within another quantifier are
+  // replaced by a Boolean variable (see below), unless the expression itself
+  // is a quantifier, which is the case when we are asked to define such a
+  // variable.
+  const bool lift_quantifiers = solver == solvert::Z3 &&
+                                lowered_expr.id() != ID_forall &&
+                                lowered_expr.id() != ID_exists;
+
   // Perform rewrites that may introduce new symbols
   for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
       it != itend;) // no ++it
   {
+    if(lift_quantifiers && (it->id() == ID_forall || it->id() == ID_exists))
+    {
+      // Z3 may report a quantified formula rather than a value for symbols
+      // whose definition contains a quantifier, see convert(const exprt &).
+      // Defining a Boolean variable per quantifier, using the encoding that
+      // works around this, keeps all other definitions quantifier-free.
+      literalt l = convert(*it);
+      it.mutate() = literal_exprt{l};
+      it.next_sibling_or_parent();
+      continue;
+    }
     if(
       auto prophecy_r_or_w_ok =
         expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(*it))

unit/solvers/smt2/smt2_conv.cpp

@@ -934,3 +934,32 @@ TEST_CASE("smt2_convt quantifier definition encoding", "[core][solvers][smt2]")
     }
   }
 }
+
+TEST_CASE(
+  "smt2_convt quantifier nested in another expression",
+  "[core][solvers][smt2]")
+{
+  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 Boolean expression containing a quantifier and the Z3 solver")
+  {
+    const std::string out =
+      convert_handle(not_exprt{quantified}, smt2_convt::solvert::Z3);
+    INFO("SMT2 output:\n" << out);
+
+    THEN("the quantifier is defined by a Boolean variable of its own")
+    {
+      // Only the definition of B0 contains the quantifier, which avoids Z3
+      // returning quantified expressions as values of other symbols.
+      const std::string assertion =
+        "(assert (let ((?def " + quant + ")) (and (=> B0 ?def) (=> ?def B0))))";
+      REQUIRE(out.find(assertion) != std::string::npos);
+      REQUIRE(out.find(quant) == out.rfind(quant));
+      REQUIRE(
+        out.find("(define-fun B1 () Bool (not B0))") != std::string::npos);
+    }
+  }
+}