Skip to content

Commit 081649e

Browse files
committed
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.
1 parent 06c2cfd commit 081649e

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ smt2_convt::smt2_convt(
9696
break;
9797

9898
case solvert::CVC4:
99+
use_array_of_bool = true;
99100
use_as_const = true;
100101
break;
101102

0 commit comments

Comments
 (0)