From dba0baa52e11abca08701b0b0a4f354e64d9a603 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 27 Nov 2010 22:22:51 +0000
Subject: added a fix for a bug in the Evaluate function.

---
 Source/Provers/Z3api/ContextLayer.cs | 33 ++++++++++++++++-----------------
 1 file 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) 
-- 
cgit v1.2.3