Skip to content

Commit 58fa61b

Browse files
Visitor: Support integer to bitvector conversion in CVC4
1 parent e7809a0 commit 58fa61b

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -438,6 +438,7 @@ private Expr normalize(Expr operator) {
438438
.put(Kind.LEQ, FunctionDeclarationKind.LTE)
439439
.put(Kind.GT, FunctionDeclarationKind.GT)
440440
.put(Kind.GEQ, FunctionDeclarationKind.GTE)
441+
.put(Kind.INT_TO_BITVECTOR, FunctionDeclarationKind.INT_TO_BV)
441442
// Bitvector theory
442443
.put(Kind.BITVECTOR_PLUS, FunctionDeclarationKind.BV_ADD)
443444
.put(Kind.BITVECTOR_SUB, FunctionDeclarationKind.BV_SUB)

0 commit comments

Comments
 (0)