diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 32 |
1 files changed, 18 insertions, 14 deletions
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;
|