From 1522ed5fa7f2ea841167ce9101359b480f19e273 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 26 Aug 2022 15:43:34 -0700 Subject: [PATCH] fix bug in genBVVecFromVec prim --- src/SAWScript/Prover/MRSolver/SMT.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 0ab447f2a3..3781ca7fab 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -260,7 +260,7 @@ smtNormPrims sc = Map.fromList -- @genCryM@ term of the new length, or vector literal into a sequence -- of @ite@s defined by the literal ("Prelude.genBVVecFromVec", - natFun $ \_m -> tvalFun $ \a -> primBVVecFromVecArg sc a $ \eith -> + PrimFun $ \_m -> tvalFun $ \a -> primBVVecFromVecArg sc a $ \eith -> PrimFun $ \_def -> natFun $ \n -> primBVTermFun sc $ \len -> Prim (do n' <- scNat sc n a' <- readBackTValueNoConfig "smtNormPrims (genBVVecFromVec)" sc a @@ -376,11 +376,11 @@ mrProvableRaw prop_term = debugPrint 2 ("SMT solver encountered a saw-core error term: " ++ msg) >> return False Right (Just cex, _) -> - debugPrint 2 "SMT solver response: not provable, with counterexample:" - >> debugPrint 3 (concatMap (\(x,v) -> - " - " ++ renderSawDoc defaultPPOpts (ppTerm defaultPPOpts (Unshared (FTermF (ExtCns x)))) ++ - " = " ++ renderSawDoc defaultPPOpts (ppFirstOrderValue defaultPPOpts v) ++ "\n") cex) - >> return False + debugPrint 2 "SMT solver response: not provable" >> + debugPrint 3 ("Counterexample:" ++ concatMap (\(x,v) -> + "\n - " ++ renderSawDoc defaultPPOpts (ppTerm defaultPPOpts (Unshared (FTermF (ExtCns x)))) ++ + " = " ++ renderSawDoc defaultPPOpts (ppFirstOrderValue defaultPPOpts v)) cex) >> + return False Right (Nothing, _) -> debugPrint 2 "SMT solver response: provable" >> return True