use bv2nat for all solvers

ucsd-progsys · Dec 20, 2024 · 7f79954 · 7f79954
1 parent 5948817
commit 7f79954
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
@@ -529,7 +529,7 @@ interpSymbols cfg =
 bv2i :: SMTSolver -> Int -> Raw
 bv2i Cvc4 _ = "bv2nat"
 bv2i Cvc5 _ = "bv2nat"
-bv2i _    n = Data.Text.pack $ printf "(_ bv2int %d)" n
+bv2i _    n = Data.Text.pack $ printf "(_ bv2nat %d)" n
 
 interpBvUop :: Symbol -> (Symbol, TheorySymbol)
 interpBvUop name = interpSym' name bvUopSort