From 39c5f29809ea2e531300d29cbee6becf752da965 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 23 Feb 2011 00:49:29 +0000
Subject: Fixes in /useArrayTheory handling

---
 Source/Provers/SMTLib/SMTLibLineariser.cs  |  6 +++++-
 Source/Provers/SMTLib/TypeDeclCollector.cs | 10 +++++++++-
 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);
           
-- 
cgit v1.2.3