Bugfixes in select-of-store axioms

1 files changed, 8 insertions, 6 deletions

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index f9e517ba..05c0ed9e 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -233,8 +233,8 @@ void ObjectInvariant()
             KnownSelectFunctions.Add(sel, true);

           }

 

-          string ax1 = "(assert (forall ";

-          string ax2 = "(assert (forall ";

+          string ax1 = "(assert (forall (";

+          string ax2 = "(assert (forall (";

 

           string argX = "", argY = "";

           string dist = "";

@@ -252,11 +252,13 @@ void ObjectInvariant()
             }

           }

           string v = " ?x" + (node.Arity - 1);

-          ax1 += "(= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argX + ") " + v + ")";

-          ax1 += ")";

+          ax1 += ") (= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argX + ") " + v + ")";

+          ax1 += "))";

 

-          ax2 += "(=> (or " + dist + ") (= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argY + ") (" + sel + " ?x0" + argY + ")))";

-          ax2 += ")";

+          if (node.Arity > 3)

+            dist = "(or " + dist + ")";

+          ax2 += ") (=> " + dist + " (= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argY + ") (" + sel + " ?x0" + argY + ")))";

+          ax2 += "))";

 

           AddDeclaration(ax1);

           AddDeclaration(ax2);