From e71b77d2c0d7d5c7bbb05ad58eaae96cd24a6d55 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Thu, 25 Apr 2013 15:20:56 +0530
Subject: AbsHoudini: Added support for /errorLimit:n, n > 1

---
 Source/BoogieDriver/BoogieDriver.cs | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'Source/BoogieDriver')

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index afc1a098..6a141fac 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -644,9 +644,6 @@ namespace Microsoft.Boogie {
               CommandLineOptions.Clo.ModelViewFile = "z3model";
               CommandLineOptions.Clo.UseArrayTheory = true;
               CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
-              // Because we use ProverEvaluate, we need to restrict counterexamples to 1 otherwise the model
-              // goes away for UseProverEvaluate
-              CommandLineOptions.Clo.ProverCCLimit = 1;
               // Declare abstract domains
               var domains = new List<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {
                   System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain),
-- 
cgit v1.2.3