Disabling non-linear integer arithmetics

src/main/scala/Config.scala

@@ -230,6 +230,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val disableNLRI: ScallopOption[Boolean] = opt[Boolean]("disableNLRI",
+    descr = "Disable non-linear integer arithetics (prover must be 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,11 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
       sys.error(s"Unexpected combination: $other")
   }
 
+  validateOpt(disableNLRI, prover) {
+    case (Some(true), n) if n != Some(Z3ProverStdIO.name) => Left(s"Option ${disableNLRI.name} is only supported with prover ${Z3ProverStdIO.name}")
+    case _ => Right(())
+  }
+
   validateOpt(counterexample, moreCompleteExhale, exhaleModeOption) {
     case (Some(_), Some(false), None) |
          (Some(_), Some(_), Some(ExhaleMode.Greedy)) =>

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.disableNLRI.getOrElse(false)) {
+      comment("We disable non-linear integer arithmetics")
+      writeLine(s"(set-option :smt.arith.nl false)")
+      readSuccess()
+    }
+  }
 }