diff options
| author |  Ken McMillan <unknown> | 2013-05-29 14:28:52 -0700 |
|---|---|---|
| committer | Ken McMillan <unknown> | 2013-05-29 14:28:52 -0700 |
| commit | a9107b72346424a3e6486622cad8284ef731ada9 (patch) | |
| tree | 749ca36db198a2c95f524d11618e118a5a028f31 /Source/Provers/SMTLib/Z3.cs | |
| parent | 3b0b6a95957a01969a85ab0b3e98de350247e0c6 (diff) | |
| parent | 45fae1a54b2b08780945c7f18ce9b8c7f9a1f763 (diff) | |
Merge changes to support Corral in fixedpoint backend
Diffstat (limited to 'Source/Provers/SMTLib/Z3.cs')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 15 |
1 files changed, 13 insertions, 2 deletions
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
|