z3 api and tests

src/main/scala/viper/gobra/frontend/Config.scala

@@ -654,7 +654,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
 
   val disableNL: ScallopOption[Boolean] = opt[Boolean](
     name = "disableNL",
-    descr = "Disable non-linear integer arithmetics. Non compatible with using Z3 via API or Carbon",
+    descr = "Disable non-linear integer arithmetics. Non compatible with Carbon",
     default = Some(ConfigDefaults.DefaultDisableNL),
     noshort = true,
   )
@@ -784,10 +784,10 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
   }
 
   addValidation {
-    if (!disableNL.toOption.contains(true) || (!z3APIMode.toOption.contains(true) && isSiliconBasedBackend)) {
+    if (!disableNL.toOption.contains(true) || isSiliconBasedBackend) {
       Right(())      
     } else {
-      Left("--disableNL is not compatible with Z3 via API or Carbon")
+      Left("--disableNL is not compatible with Carbon")
     }
   }
 

src/test/resources/regressions/examples/disableNL.gobra

@@ -1,11 +1,13 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+// ##(--disableNL)
 package pkg
 
 requires 0 <= x && x <= 10
 requires 0 <= y && y <= 10
-ensures 0 <= res && res <= 100 // would fail with --disableNL
+//:: ExpectedOutput(postcondition_error:assertion_error)
+ensures 0 <= res && res <= 100
 func f(x, y int) (res int) {
 	return x * y
 }

src/test/resources/regressions/examples/disableNL_success.gobra

@@ -0,0 +1,11 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+requires 0 <= x && x <= 10
+requires 0 <= y && y <= 10
+ensures 0 <= res && res <= 100
+func f(x, y int) (res int) {
+	return x * y
+}