From 9b03184bc671ad5a5ac68081434567b00c03e5b7 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 28 Nov 2023 12:24:43 -0800 Subject: [PATCH] comments --- Data/SBV/Core/Symbolic.hs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 12dd7e9ab..fae6bf807 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -369,9 +369,8 @@ instance Show OvOp where show (PlusOv signed) = "bv" ++ (if signed then "s" else "u") ++ "addo" show (SubOv signed) = "bv" ++ (if signed then "s" else "u") ++ "subo" show (MulOv signed) = "bv" ++ (if signed then "s" else "u") ++ "mulo" - show DivOv = "bvsdivo" - show NegOv = "bvnego" -- TODO: z3 takes the name bvnego; but this might actually be bvsnego when finally formalized - -- Reported at: https://github.com/Z3Prover/z3/issues/7010 + show DivOv = "bvsdivo" -- This is confusing, the division is called bvsdivo, but negation is bvnego + show NegOv = "bvnego" -- But SMTLib's choice is deliberate: https://groups.google.com/u/0/g/smt-lib/c/J4D99wT0aKI -- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially. data StrOp = StrConcat -- ^ Concatenation of one or more strings