Add an option to use reduce Z3's knowledge of non-linear arithmetic.

Results in more manual work, but it also produces more predictable behavior.

1 files changed, 6 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 31fe6edd..b198e224 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -41,6 +41,7 @@ namespace Microsoft.Dafny
     public bool RunAfterCompile = false;

     public bool SpillTargetCode = false;

     public bool DisallowIncludes = false;

+    public bool DisableNLarith = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -103,6 +104,11 @@ namespace Microsoft.Dafny
           DisallowIncludes = true;

           return true;

 

+        case "noNLarith":

+          DisableNLarith = true;

+          this.Z3Options.Add("NL_ARITH=false");

+          return true;

+

         default:

           break;

       }