Fixes in /useArrayTheory handling

1 files changed, 5 insertions, 1 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;

       }