From cacd7abe2152cebcf64c31f30c9c3b8cded933ae Mon Sep 17 00:00:00 2001
From: Thomas Given-Wilson <thomas.givenwilson@diffblue.com>
Date: Thu, 22 Jul 2021 14:26:07 +0100
Subject: [PATCH] Direct CVC4 to use ALL logics

This changes CVC4 to use ALL logics when solving. This has the
advantages that:
1. We will no longer receive errors when quantified expressions
   are sent to CVC4.
2. We may now solve more problems.
The disadvantages are:
A. Solving may take longer in some cases when quantifiers are
   not used.
B. CVC4 can now (more easily?) report "unknown".
Note that due to introducing quantifiers in expressions in
prior commits/work, reporting of unknown is now handled and can
be achieved with z3 already.
---
 src/solvers/smt2/smt2_conv.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 21322120357..979bd0b43fc 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -96,6 +96,7 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::CVC4:
+    logic = "ALL";
     use_array_of_bool = true;
     use_as_const = true;
     break;