diff options
| author |  qadeer <unknown> | 2010-11-27 22:22:51 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-11-27 22:22:51 +0000 |
| commit | dba0baa52e11abca08701b0b0a4f354e64d9a603 (patch) | |
| tree | 7b868d1322c0cc689c3ab5571d27943b4ad3adc1 /Source/Provers/Z3api | |
| parent | e737198c1dd35f3fa460d346bda346f2e37799a4 (diff) | |
added a fix for a bug in the Evaluate function.
Diffstat (limited to 'Source/Provers/Z3api')
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index c444e8a1..7d080eb3 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -140,6 +140,7 @@ namespace Microsoft.Boogie.Z3 Sort s = v.GetSort();
Sort boolSort = ctx.MkBoolSort();
Sort intSort = ctx.MkIntSort();
+ ArrayValue av;
if (s.Equals(boolSort))
{
@@ -157,29 +158,27 @@ namespace Microsoft.Boogie.Z3 return BigNum.FromString(ctx.GetNumeralString(v));
}
}
- else
+ else if (ctx.TryGetArrayValue(v, out av))
{
- ArrayValue av;
- if (ctx.TryGetArrayValue(v, out av))
+ List<List<int>> arrayValue = new List<List<int>>();
+ List<int> tuple;
+ for (int i = 0; i < av.Domain.Length; i++)
{
- List<List<int>> arrayValue = new List<List<int>>();
- List<int> tuple;
- for (int i = 0; i < av.Domain.Length; i++)
- {
- tuple = new List<int>();
- tuple.Add(GetPartition(av.Domain[i]));
- tuple.Add(GetPartition(av.Range[i]));
- arrayValue.Add(tuple);
- }
tuple = new List<int>();
- tuple.Add(GetPartition(av.ElseCase));
+ tuple.Add(GetPartition(av.Domain[i]));
+ tuple.Add(GetPartition(av.Range[i]));
arrayValue.Add(tuple);
- return arrayValue;
}
-
+ tuple = new List<int>();
+ tuple.Add(GetPartition(av.ElseCase));
+ arrayValue.Add(tuple);
+ return arrayValue;
+ }
+ else
+ {
+ // The term is uninterpreted; just return the partition id.
+ return GetPartition(v);
}
- Debug.Assert(false);
- return null;
}
public List<Object> PartitionToValue(Context ctx)
|