From 8c4ea73838528b78b6e992bdb9e05a0ec7fe60fe Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 15:32:30 +0200
Subject: [PATCH] refix lazy and orb
---
src/main/scala/leon/invariant/structure/FunctionUtils.scala | 4 ++--
src/main/scala/leon/laziness/LazyVerificationPhase.scala | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
index 3d5601689..eb36720b9 100644
--- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala
+++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
@@ -110,7 +110,7 @@ object FunctionUtils {
if (fd.postcondition.isDefined) {
val Lambda(_, postBody) = fd.postcondition.get
// collect all terms with question marks and convert them to a template
- val postWoQmarks = postBody match {
+ val postWoQmarks = simplifyByConstructors(postBody) match {
case And(args) if args.exists(exists(isQMark)) =>
val (tempExprs, otherPreds) = args.partition(exists(isQMark))
//println(s"Otherpreds: $otherPreds ${qmarksToTmplFunction(createAnd(tempExprs))}")
@@ -172,4 +172,4 @@ object FunctionUtils {
info
})
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index b9b5a2b7d..14b84a116 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -176,7 +176,7 @@ object LazyVerificationPhase {
def collectAntsPostTmpl(fd: FunDef) = {
val Lambda(Seq(resdef), _) = fd.postcondition.get
val (pbody, tmpl) = (fd.getPostWoTemplate, fd.template)
- val (instPost, assumptions) = pbody match {
+ val (instPost, assumptions) = simplifyByConstructors(pbody) match {
case And(args) =>
val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
(createAnd(instSpecs), createAnd(rest))
--
GitLab