Make the SMTLIB backend work again, particularly with /typeEncoding:m

1 files changed, 1 insertions, 4 deletions

diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs
index cc4f8060..78b87590 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -118,7 +118,6 @@ void ObjectInvariant()
       case impliesName:

       case iffName:

       case eqName:

-      case distinctName:

       case TRUEName:

       case FALSEName:

       case "Array":

@@ -163,8 +162,6 @@ void ObjectInvariant()
     internal const string subtypeName = "UOrdering2";

     internal const string subtypeArgsName = "UOrdering3";

 

-    internal const string distinctName = "distinct";

-

     internal const string boolTrueName = "boolTrue";

     internal const string boolFalseName = "boolFalse";

     internal const string boolIteName = "ite";

@@ -534,7 +531,7 @@ void ObjectInvariant()
         //Contract.Requires(node != null);

         //Contract.Requires(options != null);

        

-        ExprLineariser.AssertAsFormula(distinctName, options);

+        ExprLineariser.AssertAsFormula("distinct", options);

         

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);