From 7f799547b743b27f7340e4a76e96c85041b6f7bd Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sat, 21 Dec 2024 00:04:10 +0530 Subject: [PATCH] use bv2nat for all solvers --- src/Language/Fixpoint/Smt/Theories.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs index 3a1c18551..1717eba4a 100644 --- 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