From 0901edfa9185f2e2bbd331130b391dd1dda06f16 Mon Sep 17 00:00:00 2001 From: akashlal Date: Fri, 1 May 2015 23:21:22 +0530 Subject: Fix for AbsHoudini --- Source/Houdini/AbstractHoudini.cs | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'Source/Houdini') diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index fcd41656..522e8174 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -1355,6 +1355,13 @@ namespace Microsoft.Boogie.Houdini { } } + public class PredicateAbsFullElem : PredicateAbsElem + { + public PredicateAbsFullElem() + : base(1000) + { } + } + public class PredicateAbsElem : IAbstractDomain { public static class ExprExt @@ -1443,6 +1450,13 @@ namespace Microsoft.Boogie.Houdini { int DisjunctBound; bool isFalse; + public PredicateAbsElem() + { + this.conjuncts = new List(); + this.isFalse = true; + this.DisjunctBound = 3; + } + public PredicateAbsElem(int bound) { this.conjuncts = new List(); @@ -2214,8 +2228,8 @@ namespace Microsoft.Boogie.Houdini { System.Tuple.Create("HoudiniConst", HoudiniConst.GetBottom() as IAbstractDomain), System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain), System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain), - System.Tuple.Create("PredicateAbs", new PredicateAbsElem(3) as IAbstractDomain), - System.Tuple.Create("PredicateAbsFull", new PredicateAbsElem(1000) as IAbstractDomain), + System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain), + System.Tuple.Create("PredicateAbsFull", new PredicateAbsFullElem() as IAbstractDomain), System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain), System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain), System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain), -- cgit v1.2.3