From f7bdb025044d3d57898e8cb2634189beec0e00f0 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 4 Jul 2011 16:48:19 +0000
Subject: [PATCH] hardly anything
---
src/purescala/FairZ3Solver.scala | 10 +++++++---
testcases/ExprComp.scala | 2 +-
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index b13e60d9d..b34e87740 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -494,10 +494,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
- for(clause <- clauses) {
- //println("we're getting a new clause " + clause)
+ //for(clause <- clauses) {
+ //println("we're getting a new clause " + clause)
// z3.assertCnstr(toZ3Formula(z3, clause).get)
- }
+ //}
//println("The blocking guards: " + guards)
val cc = toZ3Formula(z3, And(clauses)).get
@@ -598,12 +598,14 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
if (Settings.luckyTest && !forceStop) {
// we need the model to perform the additional test
+ reporter.info(" - Running search without blocked literals (w/ lucky test)")
secondZ3SearchStopwatch.start
val (result2,m2) = assumptionsAsZ3 match {
case Some(as) => val res = z3.checkAssumptions(as: _*); (res._1, res._2)
case None => z3.checkAndGetModel()
}
secondZ3SearchStopwatch.stop
+ reporter.info(" - Finished search without blocked literals")
if (result2 == Some(false)) {
foundAnswer(Some(true))
@@ -618,12 +620,14 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
} else {
// only checking will suffice
+ reporter.info(" - Running search without blocked literals (w/o lucky test)")
secondZ3SearchStopwatch.start
val result2 = assumptionsAsZ3 match {
case Some(as) => val res = z3.checkAssumptions(as: _*); res._1
case None => z3.check()
}
secondZ3SearchStopwatch.stop
+ reporter.info(" - Finished search without blocked literals")
if (result2 == Some(false)) {
foundAnswer(Some(true))
diff --git a/testcases/ExprComp.scala b/testcases/ExprComp.scala
index ed3e9eb6d..fb36237dc 100644
--- a/testcases/ExprComp.scala
+++ b/testcases/ExprComp.scala
@@ -127,7 +127,7 @@ object ExprComp {
val vs = EStack()
val acc = EProgram()
run(compile(e, acc), vs) == Ok(NStack(eval(e), vs))
- } holds
+ } //holds
//this induction should work (at least on paper it goes ok)
--
GitLab