From ab04ef2bd635bddafeb4b334a6b6dd81c9155976 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 14:45:28 +0200
Subject: [PATCH] fix lazy
---
src/main/scala/leon/laziness/LazyVerificationPhase.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index 864f3ff28..b9b5a2b7d 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -36,7 +36,7 @@ object LazyVerificationPhase {
case fd if fd.postcondition.exists { exists(hasInstVar) } =>
// remove the conjuncts that use instrumentation vars
val Lambda(resdef, pbody) = fd.postcondition.get
- val npost = pbody match {
+ val npost = simplifyByConstructors(pbody) match {
case And(args) =>
createAnd(args.filterNot(hasInstVar))
case l: Let => // checks if the body of the let can be deconstructed as And
--
GitLab