Skip to content

Commit e824a89

Browse files
committed
Fix sort mismtach in CVC4
This fixes the sort mismatch that can occur when CVC4 expects an Array of Bool but cbmc translation produces an Array of (_ BitVec 1). Partial fix for diffblue#5970 and diffblue#5977
1 parent f9be0eb commit e824a89

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)