From dc5e51582c8fa047ed4e7f7b7ef15c59091b7899 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 25 Jun 2015 16:49:15 +0200
Subject: [PATCH] Fix obvious OptimisticGround bug
---
src/main/scala/leon/synthesis/rules/OptimisticGround.scala | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 908fdabf3..423206003 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -30,14 +30,15 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
while (result.isEmpty && i < maxTries && continue) {
val phi = andJoin(p.pc +: p.phi +: predicates)
+ val notPhi = andJoin(p.pc +: not(p.phi) +: predicates)
//println("SOLVING " + phi + " ...")
solver.solveSAT(phi) match {
case (Some(true), satModel) =>
- val newPhi = valuateWithModelIn(phi, xss, satModel)
+ val newNotPhi = valuateWithModelIn(notPhi, xss, satModel)
- //println("REFUTING " + Not(newPhi) + "...")
- solver.solveSAT(Not(newPhi)) match {
+ //println("REFUTING " + Not(newNotPhi) + "...")
+ solver.solveSAT(newNotPhi) match {
case (Some(true), invalidModel) =>
// Found as such as the xs break, refine predicates
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
--
GitLab