Skip to content
Snippets Groups Projects
Commit af5053d6 authored by Regis Blanc's avatar Regis Blanc
Browse files

fix lazy

parent 1e41ae11
No related branches found
No related tags found
No related merge requests found
...@@ -36,7 +36,7 @@ object LazyVerificationPhase { ...@@ -36,7 +36,7 @@ object LazyVerificationPhase {
case fd if fd.postcondition.exists { exists(hasInstVar) } => case fd if fd.postcondition.exists { exists(hasInstVar) } =>
// remove the conjuncts that use instrumentation vars // remove the conjuncts that use instrumentation vars
val Lambda(resdef, pbody) = fd.postcondition.get val Lambda(resdef, pbody) = fd.postcondition.get
val npost = pbody match { val npost = simplifyByConstructors(pbody) match {
case And(args) => case And(args) =>
createAnd(args.filterNot(hasInstVar)) createAnd(args.filterNot(hasInstVar))
case l: Let => // checks if the body of the let can be deconstructed as And case l: Let => // checks if the body of the let can be deconstructed as And
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment