From 45fae1a54b2b08780945c7f18ce9b8c7f9a1f763 Mon Sep 17 00:00:00 2001
From: Ken McMillan <unknown>
Date: Wed, 29 May 2013 14:24:16 -0700
Subject: Getting fixed point backend to work with Corral.

---
 Source/Provers/SMTLib/Z3.cs | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

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

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8081603e..81d5d5d1 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -259,6 +259,12 @@ namespace Microsoft.Boogie.SMTLib
                 if (options.Inspector != null)
                     options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
 
+                if (CommandLineOptions.Clo.WeakArrayTheory)
+                {
+                    // TODO: these options don't seem to exist in recent Z3
+                    // options.AddWeakSmtOption("ARRAY_WEAK", "true");
+                    // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
+                } 
             }
             else
             {
@@ -320,8 +326,13 @@ namespace Microsoft.Boogie.SMTLib
 
                 if (options.Inspector != null)
                     options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");
-
-
+                
+                if (CommandLineOptions.Clo.WeakArrayTheory)
+                {
+                    options.AddWeakSmtOption("ARRAY_WEAK", "true");
+                    options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");
+                }
+                
             }
 
             // legacy option handling
-- 
cgit v1.2.3