Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing in Simplify frontend)

1 files changed, 9 insertions, 1 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 563dec8f..9f16eb5b 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -298,7 +298,15 @@ namespace Microsoft.Boogie.SMTLib
             foreach (VCExpr e in vcTrig.Exprs) {

               Contract.Assert(e != null);

               wr.Write(" ");

-              Linearise(e, options);

+              var subPat = e;

+              var nary = e as VCExprNAry;

+              if (nary != null && (nary.Op == VCExpressionGenerator.NeqOp || nary.Op == VCExpressionGenerator.EqOp)) {

+                if (nary[0] is VCExprLiteral)

+                  subPat = nary[1];

+                else if (nary[1] is VCExprLiteral)

+                  subPat = nary[0];

+              }

+              Linearise(subPat, options);

             }

             wr.Write(")\n");

           }