From 03fea0ec749a6860d874ff00c5df93c3f171aa1c Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Wed, 11 Oct 2023 13:03:56 +0200 Subject: [PATCH] Fixing up some minor things --- src/EVM/SMT.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index 174769fd5..ea223a963 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -203,7 +203,6 @@ abstractAwayProps conf ps = runState (mapM abstrAway ps) (AbstState mempty 0) smt2Line :: Builder -> SMT2 smt2Line txt = SMT2 [txt] mempty mempty mempty -assertProps :: AbstRefineConfig -> [Prop] -> SMT2 assertProps :: Config -> [Prop] -> SMT2 -- first simplify to rewrite sload/sstore combos, then concretize&simplify assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps) @@ -212,7 +211,7 @@ assertProps conf ps = assertPropsNoSimp conf (Expr.simplifyProps ps) -- because we make use of it to verify the correctness of our simplification -- passes through property-based testing. assertPropsNoSimp :: Config -> [Prop] -> SMT2 -assertPropsNoSimp config psPreConc = +assertPropsNoSimp config ps = let encs = map propToSMT psElimAbst abstSMT = map propToSMT abstProps intermediates = declareIntermediates bufs stores in