From 36be8fc06b5d08fcf023a9b095a9ee948afcb94d Mon Sep 17 00:00:00 2001
From: Mike Barnett <mbarnett@microsoft.com>
Date: Mon, 31 Oct 2011 13:04:13 -0700
Subject: Fixed the generation of names for datatype functions to use the API
 for getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad
 axiom was being generated when no grouping had more than one occurrence.

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 32 +++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f4973efd..8d4a4256 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -483,23 +483,27 @@ namespace Microsoft.Boogie.SMTLib
           ExprLineariser.Linearise(VCExpressionGenerator.True, options);
         } else {
           var groupings = node.GroupBy(e => e.Type).Where(g => g.Count() > 1).ToArray();
+          if (groupings.Length == 0) {
+            ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+          } else {
+            if (groupings.Length > 1)
+              wr.Write("(and ");
+
+            foreach (var g in groupings) {
+              wr.Write("(distinct");
+              foreach (VCExpr e in g) {
+                Contract.Assert(e != null);
+                wr.Write(" ");
+                ExprLineariser.Linearise(e, options);
+              }
+              wr.Write(")");
+            }
 
-          if (groupings.Length > 1)
-            wr.Write("(and ");
+            if (groupings.Length > 1)
+              wr.Write(")");
 
-          foreach (var g in groupings) {
-            wr.Write("(distinct");
-            foreach (VCExpr e in g) {
-              Contract.Assert(e != null);
-              wr.Write(" ");
-              ExprLineariser.Linearise(e, options);
-            }
-            wr.Write(")");
+            wr.Write("\n");
           }
-
-          if (groupings.Length > 1)
-            wr.Write(")");
-          wr.Write("\n");
         }
 
         return true;
-- 
cgit v1.2.3