diff options
| -rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 18 |
1 files changed, 16 insertions, 2 deletions
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<Disjunct>();
+ this.isFalse = true;
+ this.DisjunctBound = 3;
+ }
+
public PredicateAbsElem(int bound)
{
this.conjuncts = new List<Disjunct>();
@@ -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),
|