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 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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;
       }
-- 
cgit v1.2.3