Skip to content

Commit

Permalink
Fixing up some minor things
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Oct 11, 2023
1 parent 3b05c85 commit 03fea0e
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/EVM/SMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down

0 comments on commit 03fea0e

Please sign in to comment.