Z3 4.8.10

.gitignore

@@ -28,3 +28,7 @@ z3/*
 # IDEA project files
 .idea/*
 *.iml
+
+# VSCode and metals
+.metals
+.vscode

README.md

@@ -1,7 +1,7 @@
 ScalaZ3 ![Build status](http://laraquad4.epfl.ch:9000/epfl-lara/ScalaZ3/status/master)
 =======
 
-This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, 2.12, and 2.13.
+This is ScalaZ3 for Z3 4.8.10 and Scala 2.10, 2.11, 2.12, and 2.13.
 
 [API documentation](https://epfl-lara.github.io/ScalaZ3/z3/index.html)
 -------------------
@@ -17,9 +17,9 @@ Run
 
     sbt +package
 
-to compile Z3 4.7.1 and cross-compile ScalaZ3 for Scala 2.10, 2.11, 2.12 and 2.13.
+to compile Z3 4.8.10 and cross-compile ScalaZ3 for Scala 2.10, 2.11, 2.12 and 2.13.
 
-The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar`
+The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.8.10.jar`
 and will contain the shared library dependencies.
 
 For testing, run
@@ -57,7 +57,7 @@ Now navigate to the scalaz3 folder and type:
 
     sbt +package
 
-The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar` and will contain the shared library
+The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.8.10.jar` and will contain the shared library
 dependencies.
 
 #### Test your package.
@@ -77,13 +77,13 @@ Using ScalaZ3
 
 ### On a single operating system / architecture
 
-Create a folder named `unmanaged` at the same level as your `build.sbt` file, and copy the JAR file in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar` into it.
+Create a folder named `unmanaged` at the same level as your `build.sbt` file, and copy the JAR file in `target/scala-2.XX/scalaz3_2.XX-4.8.10.jar` into it.
 
 Then add, the following lines to your `build.sbt` file:
 
 ```scala
-Compile / unmanagedJars += {
-  baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.7.1.jar"
+unmanagedJars in Compile += {
+  baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.8.10.jar"
 }
 ```
 

build.sbt

@@ -3,15 +3,15 @@ import ScalaZ3Build._
 lazy val root = (project in file("."))
   .settings(
     name := "ScalaZ3",
-    version := "4.7.1",
+    version := "4.8.10",
     organization := "ch.epfl.lara",
     scalacOptions ++= Seq(
       "-deprecation",
       "-unchecked",
       "-feature",
     ),
-    scalaVersion := "2.12.8",
-    crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.13.0"),
+    scalaVersion := "2.12.13",
+    crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.5"),
     libraryDependencies ++= Seq(
       "org.scalatest" %% "scalatest" % "3.0.8" % "test"
     ),
@@ -31,6 +31,7 @@ lazy val root = (project in file("."))
     Compile / compile := ((Compile / compile) dependsOn checksumTask).value,
     Test / test := ((Test / test) dependsOn (Compile / Keys.`package`)).value,
     Test / compile := ((Test / compile) dependsOn (Compile / Keys.`package`)).value,
+    Test / testOnly := ((Test / testOnly) dependsOn (Compile / Keys.`package`)).evaluated,
     Test / internalDependencyClasspath := testClasspath.value,
     Compile / packageBin / mappings := newMappingsTask.value,
   )

project/Build.scala

@@ -6,7 +6,7 @@ import scala.sys.process._
 object ScalaZ3Build {
 
   lazy val z3SourceRepo = "https://github.com/Z3Prover/z3.git"
-  lazy val z3SourceTag  = "z3-4.7.1"
+  lazy val z3SourceTag  = "z3-4.8.10"
 
   lazy val PS = java.io.File.pathSeparator
   lazy val DS = java.io.File.separator

src/main/scala/z3/scala/Z3Context.scala

@@ -1024,24 +1024,6 @@ sealed class Z3Context(val config: Map[String, String]) {
     res
   }
 
-  // XXX: this is a HUGE hack to get around the fact that the Z3 api doesn't
-  //      provide a handle to the absolute value function.
-  def getAbsFuncDecl(): Z3FuncDecl = {
-    val ast = parseSMTLIB2String("""
-      (declare-fun x () Int)
-      (declare-fun y () Int)
-      (assert (= y (abs x)))
-    """)
-
-    getASTKind(ast) match {
-      case Z3AppAST(_, Seq(_, absAst)) => getASTKind(absAst) match {
-        case Z3AppAST(decl, _) => decl
-        case c => error("Unexpected ast kind " + c)
-      }
-      case c => error("Unexpected ast kind " + c)
-    }
-  }
-
   // Parser interface
   private def parseSMTLIB2(file: Boolean, str: String) : Z3AST = {
     if(file) {

src/main/scala/z3/scala/Z3Optimizer.scala

@@ -67,7 +67,7 @@ class Z3Optimizer private[z3](val ptr: Long, val context: Z3Context) extends Z3O
   private[this] var lastResult: Option[Boolean] = None
 
   def check(): Option[Boolean] = {
-    val res = i2ob(Native.optimizeCheck(context.ptr, this.ptr))
+    val res = i2ob(Native.optimizeCheck(context.ptr, this.ptr, 0, null))
     lastResult = res
     res
   }