Merge pull request #783 from viperproject/dspil_disable_nlri

Option disabling non-linear integer arithmetic

Author: Dspil

src/main/scala/Config.scala

@@ -230,6 +230,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val disableNL: ScallopOption[Boolean] = opt[Boolean]("disableNL",
+    descr = "Disable non-linear integer arithmetic when using Z3",
+    default = Some(false),
+    noshort = true
+  )
+
   private val rawProverSaturationTimeout = opt[Int]("proverSaturationTimeout",
     descr = (  "Timeout (in ms) used for the prover's state saturation calls (default: 100). "
              + "A timeout of 0 disables all saturation checks."
@@ -813,6 +819,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
+  validateOpt(disableNL, prover) {
+    case (Some(true), n) if (n != Some(Z3ProverStdIO.name) && n != Some(Z3ProverAPI.name)) =>
+        Left(s"Option ${disableNL.name} is only supported with Z3")
+    case _ => Right(())
+  }
+
   validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
     case (Some(_), Some(false), None) |
          (Some(_), Some(_), Some(ExhaleMode.Greedy)) =>

src/main/scala/decider/Z3ProverAPI.scala

@@ -135,6 +135,9 @@ class Z3ProverAPI(uniqueId: String,
       case (k, v) =>
         params.add(removeSmtPrefix(k), v)
     }
+    if (Verifier.config.disableNL.getOrElse(false)) {
+      params.add("arith.nl", false)
+    }
     val userProvidedArgs = Verifier.config.proverConfigArgs
     prover = ctx.mkSolver()
     val descrs = prover.getParameterDescriptions

src/main/scala/decider/Z3ProverStdIO.scala

@@ -65,5 +65,12 @@ class Z3ProverStdIO(uniqueId: String,
     Paths.get(Verifier.config.z3Exe)
   }
 
-  override def emitSettings(contents: Iterable[String]): Unit = emit(contents)
+  override def emitSettings(contents: Iterable[String]): Unit = {
+    emit(contents)
+    if (Verifier.config.disableNL.getOrElse(false)) {
+      comment("We disable non-linear integer arithmetic")
+      writeLine(s"(set-option :smt.arith.nl false)")
+      readSuccess()
+    }
+  }
 }

src/test/resources/misc/disableNL.vpr

@@ -0,0 +1,7 @@
+method f(x: Int, y: Int) returns (res: Int)
+  requires 0 <= x <= 10
+  requires 0 <= y <= 10
+  ensures 0 <= res <= 100 // this fails with --disableNL
+{
+  res := x * y
+}