From 081649e737dc1ff42a4304ed6a2ca85625ec342c Mon Sep 17 00:00:00 2001
From: Thomas Given-Wilson <thomas.givenwilson@diffblue.com>
Date: Mon, 28 Jun 2021 14:54:26 +0100
Subject: [PATCH] Fix bool versus bitvec 1 sort mismtach for CVC4

This fixes a sort mismatch that can occur in CVC4 where an
array of booleans is translated into an array of (_ bitvec 1)
which is then a mismatch when CVC4 expects and can handle an
Array of Bool.
---
 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 d9da852ab62..1226aebd029 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:
+    use_array_of_bool = true;
     use_as_const = true;
     break;