Fixes in /useArrayTheory handling

2 files changed, 14 insertions, 2 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 4cec5ad4..563dec8f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -512,9 +512,11 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       public bool VisitSelectOp(VCExprNAry node, LineariserOptions options)

-      {

+      {        

         var name = SimplifyLikeExprLineariser.SelectOpName(node);

         name = ExprLineariser.Namer.GetQuotedName(name, name);

+        if (CommandLineOptions.Clo.UseArrayTheory)

+          name = "select";

         WriteApplication(name, node, options);

         return true;

       }

@@ -523,6 +525,8 @@ namespace Microsoft.Boogie.SMTLib
       {

         var name = SimplifyLikeExprLineariser.StoreOpName(node);

         name = ExprLineariser.Namer.GetQuotedName(name, name);

+        if (CommandLineOptions.Clo.UseArrayTheory)

+          name = "store";

         WriteApplication(name, node, options);

         return true;

       }

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 0a03e4ab..b98378b2 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -196,6 +196,10 @@ void ObjectInvariant()
     private void RegisterSelect(VCExprNAry node)

     {

       RegisterType(node[0].Type);

+

+      if (CommandLineOptions.Clo.UseArrayTheory)

+        return;

+

       string name = SimplifyLikeExprLineariser.SelectOpName(node);

       name = Namer.GetQuotedName(name, name);

 

@@ -209,6 +213,10 @@ void ObjectInvariant()
     private void RegisterStore(VCExprNAry node)

     {

       RegisterType(node.Type);        // this is the map type, registering it should register also the index and value types

+

+      if (CommandLineOptions.Clo.UseArrayTheory)

+        return;

+

       string name = SimplifyLikeExprLineariser.StoreOpName(node);

       name = Namer.GetQuotedName(name, name);

 

@@ -216,7 +224,7 @@ void ObjectInvariant()
         string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";

         AddDeclaration(decl);

 

-        if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {

+        if (CommandLineOptions.Clo.MonomorphicArrays) {

           var sel = SimplifyLikeExprLineariser.SelectOpName(node);

           sel = Namer.GetQuotedName(sel, sel);