From 199e9aa6272e9c015665856a5f3196111e783b6f Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 23 Nov 2012 17:21:17 +0100
Subject: [PATCH] Work in progress.
---
src/main/scala/leon/Settings.scala | 2 +-
src/main/scala/leon/plugin/LeonPlugin.scala | 4 ++--
src/main/scala/leon/verification/AnalysisPhase.scala | 4 ++++
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 5e2585eb5..f643c3a24 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -18,7 +18,7 @@ object Settings {
var useCores : Boolean = false
var pruneBranches : Boolean = false
var solverTimeout : Option[Int] = None
- var luckyTest : Boolean = true
+ //var luckyTest : Boolean = true
var verifyModel : Boolean = true
var useQuickCheck : Boolean = false
var useParallel : Boolean = false
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index afc5fa35d..bdba7fb64 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -35,7 +35,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
" --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
- " --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
+ //" --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
" --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
" --debug=[1-5] Debug level" + "\n" +
" --tags=t1:... Filter out debug information that are not of one of the given tags" + "\n" +
@@ -63,7 +63,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
case "cores" => leon.Settings.useCores = true
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
- case "noLuckyTests" => leon.Settings.luckyTest = false
+ //case "noLuckyTests" => leon.Settings.luckyTest = false
case "noverifymodel" => leon.Settings.verifyModel = false
case "imperative" => leon.Settings.synthesis = false;
leon.Settings.transformProgram = true;
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 726a7922a..12953a93b 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -7,6 +7,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
+ override def definedOptions = Set(
+ LeonFlagOptionDef("no-luck", "--no-luck", "Disable early model detection in solving loop.")
+ )
+
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
new Analysis(program, ctx.reporter).analyse
}
--
GitLab