Fix a bug in distinct() encoding

2 files changed, 3 insertions, 3 deletions

diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs
index 3e3e5ed2..cc4f8060 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -549,7 +549,7 @@ void ObjectInvariant()
           wr.Write("($true ");

           foreach (VCExpr e in node) {

             for (var i = 0; i < bits; ++i) {

-              var neg = (cnt & (1 >> i)) != 0 ? "~" : "";

+              var neg = (cnt & (1 << i)) != 0 ? "~" : "";

               wr.Write(" & {0}distinct__f__{1}(", neg, i);

               ExprLineariser.LineariseAsTerm(e, options);

               wr.Write(")");

diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs
index 0d0eb19a..beecf660 100644
--- a/Source/Provers/TPTP/TypeDeclCollector.cs
+++ b/Source/Provers/TPTP/TypeDeclCollector.cs
@@ -113,10 +113,10 @@ void ObjectInvariant()
             }

 

             string ax1 = "fof(selectEq" + id + ", axiom, ! [M,V," + xS + "] : (" +

-                             string.Format("{0}({1}(M,{2},V),{2}) = V", sel, name, xS) + ")).";

+                             string.Format("{0}({1}(M,{2},V),{2}) {3} V", sel, name, xS, eq) + ")).";

             string ax2 = "fof(selectNeq" + id + ", axiom, ! [M,V," + xS + "," + yS + "] : (" +

                              string.Format("( {0} ) => ", dist) +

-                             string.Format("{0}({1}(M,{2},V),{3}) = {0}(M,{3})", sel, name, xS, yS) + ")).";

+                             string.Format("{0}({1}(M,{2},V),{3}) {4} {0}(M,{3})", sel, name, xS, yS, eq) + ")).";

 

             AddDeclaration(ax1);

             AddDeclaration(ax2);