From 93e49749af27e816a6924e74cff620e589412c7b Mon Sep 17 00:00:00 2001 From: akashlal Date: Fri, 19 Apr 2013 11:02:07 +0530 Subject: AbsHoudini: Added SCC-based worklist, bug-fix for inline attribute, intervals domain --- Source/BoogieDriver/BoogieDriver.cs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9ef365c0..0ffa5619 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -644,13 +644,15 @@ 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; - CommandLineOptions.Clo.UseSubsumption = CommandLineOptions.SubsumptionOption.Never; - // Declare abstract domains var domains = new List>(new System.Tuple[] { + System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain), System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), - System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) + System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), + System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) }); domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2)); -- cgit v1.2.3