From a3ac39ae49189528637b4681bd9698c0d8d5091e Mon Sep 17 00:00:00 2001
From: Mario Bucev <mario.bucev@epfl.ch>
Date: Wed, 15 Dec 2021 13:13:22 +0100
Subject: [PATCH] Z3 4.8.14

---
 README.md                                 | 14 ++--
 build.sbt                                 |  7 +-
 project/Build.scala                       | 23 +++++-
 src/main/scala/z3/scala/Z3Context.scala   | 51 +++++-------
 src/main/scala/z3/scala/Z3DeclKind.scala  | 98 ++++++++++++-----------
 src/main/scala/z3/scala/Z3Optimizer.scala |  2 +-
 src/main/scala/z3/scala/Z3Solver.scala    | 22 ++---
 src/main/scala/z3/scala/Z3Sort.scala      |  8 +-
 src/main/scala/z3/scala/dsl/Trees.scala   | 12 +--
 src/main/scala/z3/scala/dsl/package.scala | 40 ++++-----
 src/test/scala/z3/scala/ADTs.scala        |  8 +-
 src/test/scala/z3/scala/Abs.scala         | 11 +--
 src/test/scala/z3/scala/Arrays.scala      |  8 +-
 src/test/scala/z3/scala/Core.scala        | 18 ++---
 src/test/scala/z3/scala/IntArith.scala    |  8 +-
 src/test/scala/z3/scala/NQueens.scala     |  6 +-
 src/test/scala/z3/scala/Optimizer.scala   |  8 +-
 src/test/scala/z3/scala/Quantifiers.scala | 26 +++---
 src/test/scala/z3/scala/SatSolver.scala   | 16 ++--
 src/test/scala/z3/scala/Sequences.scala   | 18 ++---
 src/test/scala/z3/scala/Sets.scala        |  6 +-
 z3_mk_abs.patch                           | 48 +++++++++++
 22 files changed, 261 insertions(+), 197 deletions(-)
 create mode 100644 z3_mk_abs.patch

diff --git a/README.md b/README.md
index 20a1dd4..f746ca0 100644
--- a/README.md
+++ b/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.14 and Scala 2.10, 2.11, 2.12, and 2.13.
 
 [API documentation](https://epfl-lara.github.io/ScalaZ3/z3/index.html)
 -------------------
@@ -9,7 +9,7 @@ This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, 2.12, and 2.13.
 Compiling ScalaZ3
 -----------------
 
-You should have Java and SBT 1.2.x installed.
+You should have Java and SBT 1.5.x installed.
 
 ### Mac & Unix
 
@@ -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.14 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.14.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.14.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.14.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"
+  baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.8.14.jar"
 }
 ```
 
diff --git a/build.sbt b/build.sbt
index 9af358d..65f7440 100644
--- a/build.sbt
+++ b/build.sbt
@@ -3,15 +3,15 @@ import ScalaZ3Build._
 lazy val root = (project in file("."))
   .settings(
     name := "ScalaZ3",
-    version := "4.7.1",
+    version := "4.8.14",
     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.13.6"),
     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,
   )
diff --git a/project/Build.scala b/project/Build.scala
index 3a011d9..86669d4 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -1,12 +1,15 @@
 import sbt._
 import sbt.Keys._
 import org.eclipse.jgit.api._
+import org.eclipse.jgit.treewalk.filter.PathFilter
+
+import java.io.{FileInputStream, InputStream}
 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.14"
 
   lazy val PS = java.io.File.pathSeparator
   lazy val DS = java.io.File.separator
@@ -124,6 +127,24 @@ object ScalaZ3Build {
       .setName(z3SourceTag)
       .call()
 
+    val diffs = Git.open(z3Path.asFile)
+      .diff()
+      .setPathFilter(PathFilter.create("src/api/"))
+      .call()
+    if (diffs.isEmpty) {
+      s.log.info(s"Applying mk_abs API patch...")
+      var is: InputStream = null
+      try {
+        is = new FileInputStream(new File("z3_mk_abs.patch"))
+        Git.open(z3Path.asFile)
+          .apply()
+          .setPatch(is)
+          .call()
+      } finally {
+        if (is != null) is.close()
+      }
+    }
+
     val hashFile = z3Path / ".build-hash"
 
     def computeHash(): String = {
diff --git a/src/main/scala/z3/scala/Z3Context.scala b/src/main/scala/z3/scala/Z3Context.scala
index edd2ec5..10f85c6 100644
--- a/src/main/scala/z3/scala/Z3Context.scala
+++ b/src/main/scala/z3/scala/Z3Context.scala
@@ -236,7 +236,7 @@ sealed class Z3Context(val config: Map[String, String]) {
 
       val (consFuns, unzippedOnce) = zipped.unzip
       val (testFuns, selectorFunss) = unzippedOnce.unzip
-  
+
       (new Z3Sort(sort, this), consFuns, testFuns, selectorFunss)
     }
   }
@@ -265,7 +265,7 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def mkIntConst(symbol: Z3Symbol) : Z3AST = {
-    mkConst(symbol, mkIntSort)
+    mkConst(symbol, mkIntSort())
   }
 
   def mkIntConst(s: String) : Z3AST = {
@@ -273,7 +273,7 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def mkBoolConst(symbol: Z3Symbol) : Z3AST = {
-    mkConst(symbol, mkBoolSort)
+    mkConst(symbol, mkBoolSort())
   }
 
   def mkBoolConst(s: String) : Z3AST = {
@@ -301,11 +301,11 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def mkFreshIntConst(prefix: String) : Z3AST = {
-    mkFreshConst(prefix, mkIntSort)
+    mkFreshConst(prefix, mkIntSort())
   }
 
   def mkFreshBoolConst(prefix: String) : Z3AST = {
-    mkFreshConst(prefix, mkBoolSort)
+    mkFreshConst(prefix, mkBoolSort())
   }
 
   def mkFreshFuncDecl(prefix: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort) : Z3FuncDecl = {
@@ -328,7 +328,7 @@ sealed class Z3Context(val config: Map[String, String]) {
     if(args.size == 0) {
       throw new IllegalArgumentException("mkDistinct needs at least one argument")
     } else if(args.size == 1) {
-      mkTrue
+      mkTrue()
     } else {
       new Z3AST(Native.mkDistinct(this.ptr, args.length, toPtrArray(args)), this)
     }
@@ -444,6 +444,10 @@ sealed class Z3Context(val config: Map[String, String]) {
     new Z3AST(Native.mkInt2real(this.ptr, ast.ptr), this)
   }
 
+  def mkAbs(ast: Z3AST) : Z3AST = {
+    new Z3AST(Native.mkAbs(this.ptr, ast.ptr), this)
+  }
+
   def mkReal2Int(ast: Z3AST) : Z3AST = {
     new Z3AST(Native.mkReal2int(this.ptr, ast.ptr), this)
   }
@@ -642,7 +646,7 @@ sealed class Z3Context(val config: Map[String, String]) {
   def mkInt(value: Int, sort: Z3Sort) : Z3AST = {
     new Z3AST(Native.mkInt(this.ptr, value, sort.ptr), this)
   }
-  
+
   def mkReal(numerator: Int, denominator: Int) : Z3AST = {
     new Z3AST(Native.mkReal(this.ptr, numerator, denominator), this)
   }
@@ -875,6 +879,7 @@ sealed class Z3Context(val config: Map[String, String]) {
       case OpUMinus => mkUnaryMinus(mkFreshConst("x", sorts(0)))
       case OpMul => mkMul(sorts.map(mkFreshConst("x", _)) : _*)
       case OpDiv => mkDiv(mkFreshConst("a", sorts(0)), mkFreshConst("b", sorts(1)))
+      case OpAbs => mkAbs(mkFreshConst("x", sorts(0)))
       case _ => error("Unexpected decl kind " + op)
     }
 
@@ -938,23 +943,23 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def getIndexValue(ast: Z3AST) : Int = {
-    return Native.getIndexValue(this.ptr, ast.ptr)
+    Native.getIndexValue(this.ptr, ast.ptr)
   }
 
   def isQuantifierForall(ast: Z3AST) : Boolean = {
-    return Native.isQuantifierForall(this.ptr, ast.ptr)
+    Native.isQuantifierForall(this.ptr, ast.ptr)
   }
 
   def getQuantifierBody(ast: Z3AST) : Z3AST = {
-    return new Z3AST(Native.getQuantifierBody(this.ptr, ast.ptr), this)
+    new Z3AST(Native.getQuantifierBody(this.ptr, ast.ptr), this)
   }
 
   def getQuantifierBoundName(ast: Z3AST, i: Int) : Z3Symbol = {
-    return new Z3Symbol(Native.getQuantifierBoundName(this.ptr, ast.ptr, i), this)
+    new Z3Symbol(Native.getQuantifierBoundName(this.ptr, ast.ptr, i), this)
   }
 
   def getQuantifierNumBound(ast: Z3AST) : Int = {
-    return Native.getQuantifierNumBound(this.ptr, ast.ptr)
+    Native.getQuantifierNumBound(this.ptr, ast.ptr)
   }
 
   def getDeclKind(funcDecl: Z3FuncDecl) : Z3DeclKind = {
@@ -1024,22 +1029,8 @@ 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)
-    }
+    getFuncDecl(OpAbs, mkIntSort())
   }
 
   // Parser interface
@@ -1095,7 +1086,7 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def simplifyAst(ast : Z3AST) : Z3AST = {
-    return new Z3AST(Native.simplify(this.ptr, ast.ptr), this);
+    new Z3AST(Native.simplify(this.ptr, ast.ptr), this);
   }
 
   def mkForAllConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST) : Z3AST = mkQuantifierConst(true, weight, patterns, bounds, body)
@@ -1118,11 +1109,11 @@ sealed class Z3Context(val config: Map[String, String]) {
   }
 
   def mkTactic(name: String) : Z3Tactic = {
-    return new Z3Tactic(Native.mkTactic(this.ptr, name), this)
+    new Z3Tactic(Native.mkTactic(this.ptr, name), this)
   }
 
   def mkTacticAndThen(tactic1: Z3Tactic, tactic2: Z3Tactic) : Z3Tactic = {
-    return new Z3Tactic(Native.tacticAndThen(this.ptr, tactic1.ptr, tactic2.ptr), this)
+    new Z3Tactic(Native.tacticAndThen(this.ptr, tactic1.ptr, tactic2.ptr), this)
   }
 
   def mkSolver() : Z3Solver = {
diff --git a/src/main/scala/z3/scala/Z3DeclKind.scala b/src/main/scala/z3/scala/Z3DeclKind.scala
index 6dae8cf..bbef95d 100644
--- a/src/main/scala/z3/scala/Z3DeclKind.scala
+++ b/src/main/scala/z3/scala/Z3DeclKind.scala
@@ -37,19 +37,20 @@ object OpToReal extends Z3DeclKind (Z3_decl_kind.Z3_OP_TO_REAL.toInt)
 object OpToInt  extends Z3DeclKind (Z3_decl_kind.Z3_OP_TO_INT.toInt)
 object OpIsInt  extends Z3DeclKind (Z3_decl_kind.Z3_OP_IS_INT.toInt)
 object OpPower  extends Z3DeclKind (Z3_decl_kind.Z3_OP_POWER.toInt)  // NEW in ScalaZ3 3.0
+object OpAbs    extends Z3DeclKind (Z3_decl_kind.Z3_OP_ABS.toInt)  // NEW in ScalaZ3 4.8.12
 
 // Arrays & Sets
-object OpStore         extends Z3DeclKind (Z3_decl_kind.Z3_OP_STORE.toInt)        
-object OpSelect        extends Z3DeclKind (Z3_decl_kind.Z3_OP_SELECT.toInt)       
-object OpConstArray    extends Z3DeclKind (Z3_decl_kind.Z3_OP_CONST_ARRAY.toInt)   
-object OpArrayMap      extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_MAP.toInt)     
-object OpArrayDefault  extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_DEFAULT.toInt) 
-object OpSetUnion      extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_UNION.toInt)     
-object OpSetIntersect  extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_INTERSECT.toInt) 
+object OpStore         extends Z3DeclKind (Z3_decl_kind.Z3_OP_STORE.toInt)
+object OpSelect        extends Z3DeclKind (Z3_decl_kind.Z3_OP_SELECT.toInt)
+object OpConstArray    extends Z3DeclKind (Z3_decl_kind.Z3_OP_CONST_ARRAY.toInt)
+object OpArrayMap      extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_MAP.toInt)
+object OpArrayDefault  extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_DEFAULT.toInt)
+object OpSetUnion      extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_UNION.toInt)
+object OpSetIntersect  extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_INTERSECT.toInt)
 object OpSetDifference extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_DIFFERENCE.toInt)
 object OpSetComplement extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_COMPLEMENT.toInt)
-object OpSetSubset     extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_SUBSET.toInt)    
-object OpAsArray       extends Z3DeclKind (Z3_decl_kind.Z3_OP_AS_ARRAY.toInt)      
+object OpSetSubset     extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_SUBSET.toInt)
+object OpAsArray       extends Z3DeclKind (Z3_decl_kind.Z3_OP_AS_ARRAY.toInt)
 object OpArrayExt      extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_EXT.toInt) // NEW in ScalaZ3 3.0
 
 // Bit-vectors
@@ -262,50 +263,51 @@ object Z3DeclKind {
   }
 
   def fromZ3(kind: Z3_decl_kind): Z3DeclKind = kind match {
-    case Z3_decl_kind.Z3_OP_TRUE  => OpTrue 
-    case Z3_decl_kind.Z3_OP_FALSE => OpFalse 
-    case Z3_decl_kind.Z3_OP_EQ => OpEq 
-    case Z3_decl_kind.Z3_OP_DISTINCT => OpDistinct 
-    case Z3_decl_kind.Z3_OP_ITE => OpITE 
-    case Z3_decl_kind.Z3_OP_AND => OpAnd 
-    case Z3_decl_kind.Z3_OP_OR => OpOr 
-    case Z3_decl_kind.Z3_OP_IFF => OpIff 
-    case Z3_decl_kind.Z3_OP_XOR => OpXor 
-    case Z3_decl_kind.Z3_OP_NOT => OpNot 
-    case Z3_decl_kind.Z3_OP_IMPLIES => OpImplies 
+    case Z3_decl_kind.Z3_OP_TRUE  => OpTrue
+    case Z3_decl_kind.Z3_OP_FALSE => OpFalse
+    case Z3_decl_kind.Z3_OP_EQ => OpEq
+    case Z3_decl_kind.Z3_OP_DISTINCT => OpDistinct
+    case Z3_decl_kind.Z3_OP_ITE => OpITE
+    case Z3_decl_kind.Z3_OP_AND => OpAnd
+    case Z3_decl_kind.Z3_OP_OR => OpOr
+    case Z3_decl_kind.Z3_OP_IFF => OpIff
+    case Z3_decl_kind.Z3_OP_XOR => OpXor
+    case Z3_decl_kind.Z3_OP_NOT => OpNot
+    case Z3_decl_kind.Z3_OP_IMPLIES => OpImplies
     case Z3_decl_kind.Z3_OP_OEQ => OpOEq
 
-    case Z3_decl_kind.Z3_OP_ANUM => OpANum 
-    case Z3_decl_kind.Z3_OP_AGNUM => OpAGNum 
-    case Z3_decl_kind.Z3_OP_LE => OpLE 
-    case Z3_decl_kind.Z3_OP_GE => OpGE 
-    case Z3_decl_kind.Z3_OP_LT => OpLT 
-    case Z3_decl_kind.Z3_OP_GT => OpGT 
-    case Z3_decl_kind.Z3_OP_ADD => OpAdd 
-    case Z3_decl_kind.Z3_OP_SUB => OpSub 
-    case Z3_decl_kind.Z3_OP_UMINUS => OpUMinus 
-    case Z3_decl_kind.Z3_OP_MUL => OpMul 
-    case Z3_decl_kind.Z3_OP_DIV => OpDiv 
-    case Z3_decl_kind.Z3_OP_IDIV => OpIDiv 
-    case Z3_decl_kind.Z3_OP_REM => OpRem 
-    case Z3_decl_kind.Z3_OP_MOD => OpMod 
-    case Z3_decl_kind.Z3_OP_TO_REAL => OpToReal 
-    case Z3_decl_kind.Z3_OP_TO_INT => OpToInt 
-    case Z3_decl_kind.Z3_OP_IS_INT => OpIsInt 
-    case Z3_decl_kind.Z3_OP_POWER => OpPower 
-
-    case Z3_decl_kind.Z3_OP_STORE => OpStore 
-    case Z3_decl_kind.Z3_OP_SELECT => OpSelect 
-    case Z3_decl_kind.Z3_OP_CONST_ARRAY => OpConstArray 
+    case Z3_decl_kind.Z3_OP_ANUM => OpANum
+    case Z3_decl_kind.Z3_OP_AGNUM => OpAGNum
+    case Z3_decl_kind.Z3_OP_LE => OpLE
+    case Z3_decl_kind.Z3_OP_GE => OpGE
+    case Z3_decl_kind.Z3_OP_LT => OpLT
+    case Z3_decl_kind.Z3_OP_GT => OpGT
+    case Z3_decl_kind.Z3_OP_ADD => OpAdd
+    case Z3_decl_kind.Z3_OP_SUB => OpSub
+    case Z3_decl_kind.Z3_OP_UMINUS => OpUMinus
+    case Z3_decl_kind.Z3_OP_MUL => OpMul
+    case Z3_decl_kind.Z3_OP_DIV => OpDiv
+    case Z3_decl_kind.Z3_OP_IDIV => OpIDiv
+    case Z3_decl_kind.Z3_OP_REM => OpRem
+    case Z3_decl_kind.Z3_OP_MOD => OpMod
+    case Z3_decl_kind.Z3_OP_TO_REAL => OpToReal
+    case Z3_decl_kind.Z3_OP_TO_INT => OpToInt
+    case Z3_decl_kind.Z3_OP_IS_INT => OpIsInt
+    case Z3_decl_kind.Z3_OP_POWER => OpPower
+    case Z3_decl_kind.Z3_OP_ABS => OpAbs
+
+    case Z3_decl_kind.Z3_OP_STORE => OpStore
+    case Z3_decl_kind.Z3_OP_SELECT => OpSelect
+    case Z3_decl_kind.Z3_OP_CONST_ARRAY => OpConstArray
     case Z3_decl_kind.Z3_OP_ARRAY_MAP => OpArrayMap
     case Z3_decl_kind.Z3_OP_ARRAY_DEFAULT => OpArrayDefault
-    case Z3_decl_kind.Z3_OP_SET_UNION => OpSetUnion 
-    case Z3_decl_kind.Z3_OP_SET_INTERSECT => OpSetIntersect 
-    case Z3_decl_kind.Z3_OP_SET_DIFFERENCE => OpSetDifference 
-    case Z3_decl_kind.Z3_OP_SET_COMPLEMENT => OpSetComplement 
+    case Z3_decl_kind.Z3_OP_SET_UNION => OpSetUnion
+    case Z3_decl_kind.Z3_OP_SET_INTERSECT => OpSetIntersect
+    case Z3_decl_kind.Z3_OP_SET_DIFFERENCE => OpSetDifference
+    case Z3_decl_kind.Z3_OP_SET_COMPLEMENT => OpSetComplement
     case Z3_decl_kind.Z3_OP_SET_SUBSET => OpSetSubset
-    case Z3_decl_kind.Z3_OP_AS_ARRAY => OpAsArray 
-    case Z3_decl_kind.Z3_OP_ARRAY_EXT => OpArrayExt 
+    case Z3_decl_kind.Z3_OP_AS_ARRAY => OpAsArray
+    case Z3_decl_kind.Z3_OP_ARRAY_EXT => OpArrayExt
 
     case Z3_decl_kind.Z3_OP_BNUM => OpBNum
     case Z3_decl_kind.Z3_OP_BIT1 => OpBit1
diff --git a/src/main/scala/z3/scala/Z3Optimizer.scala b/src/main/scala/z3/scala/Z3Optimizer.scala
index be342b5..047ff31 100644
--- a/src/main/scala/z3/scala/Z3Optimizer.scala
+++ b/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
   }
diff --git a/src/main/scala/z3/scala/Z3Solver.scala b/src/main/scala/z3/scala/Z3Solver.scala
index 332adb0..2f7f806 100644
--- a/src/main/scala/z3/scala/Z3Solver.scala
+++ b/src/main/scala/z3/scala/Z3Solver.scala
@@ -66,7 +66,7 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
   }
 
   def getNumScopes() = {
-    Native.solverGetNumScopes(context.ptr, this.ptr)  
+    Native.solverGetNumScopes(context.ptr, this.ptr)
   }
 
   def incRef(): Unit = {
@@ -106,9 +106,9 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
 
   private[z3] def checkAndGetAllModels(): Iterator[Z3Model] = {
     new Iterator[Z3Model] {
-      var constraints: Z3AST = context.mkTrue
+      var constraints: Z3AST = context.mkTrue()
       var nextModel: Option[Option[Z3Model]] = None
-      
+
       override def hasNext: Boolean =  nextModel match {
         case None =>
           // Check whether there are any more models
@@ -119,7 +119,7 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
           val toReturn = (result match {
             case (Some(true), m) =>
               nextModel = Some(Some(m))
-              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue){
+              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue()){
                 (acc, s) => context.mkAnd(acc, context.mkEq(s._1(), s._2))
               }
               constraints = context.mkAnd(constraints, context.mkNot(newConstraints))
@@ -145,7 +145,7 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
           pop(1)
           val toReturn = (result match {
             case (Some(true), m) =>
-              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue){
+              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue()){
                 (acc, s) => context.mkAnd(acc, context.mkEq(s._1(), s._2))
               }
               constraints = context.mkAnd(constraints, context.mkNot(newConstraints))
@@ -154,7 +154,7 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
               throw new Exception("Requesting a new model while there are no more models.")
           })
           toReturn
-        case Some(Some(m)) => 
+        case Some(Some(m)) =>
           nextModel = None
           m
         case Some(None) => throw new Exception("Requesting a new model while there are no more models.")
@@ -164,9 +164,9 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
 
   private[z3] def checkAndGetAllEventualModels(): Iterator[(Option[Boolean], Z3Model)] = {
     new Iterator[(Option[Boolean], Z3Model)] {
-      var constraints: Z3AST = context.mkTrue
+      var constraints: Z3AST = context.mkTrue()
       var nextModel: Option[Option[(Option[Boolean],Z3Model)]] = None
-      
+
       override def hasNext: Boolean =  nextModel match {
         case None =>
           // Check whether there are any more models
@@ -180,7 +180,7 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
               false
             case (outcome, m) =>
               nextModel = Some(Some((outcome, m)))
-              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue){
+              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue()){
                 (acc, s) => context.mkAnd(acc, context.mkEq(s._1(), s._2))
               }
               constraints = context.mkAnd(constraints, context.mkNot(newConstraints))
@@ -202,14 +202,14 @@ class Z3Solver private[z3](val ptr: Long, val context: Z3Context) extends Z3Obje
             case (Some(false), _) =>
               throw new Exception("Requesting a new model while there are no more models.")
             case (outcome, m) =>
-              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue){
+              val newConstraints = m.getConstInterpretations.foldLeft(context.mkTrue()){
                 (acc, s) => context.mkAnd(acc, context.mkEq(s._1(), s._2))
               }
               constraints = context.mkAnd(constraints, context.mkNot(newConstraints))
               (outcome, m)
           })
           toReturn
-        case Some(Some((outcome, m))) => 
+        case Some(Some((outcome, m))) =>
           nextModel = None
           (outcome, m)
         case Some(None) => throw new Exception("Requesting a new model while there are no more models.")
diff --git a/src/main/scala/z3/scala/Z3Sort.scala b/src/main/scala/z3/scala/Z3Sort.scala
index 9ab7f37..68790e9 100644
--- a/src/main/scala/z3/scala/Z3Sort.scala
+++ b/src/main/scala/z3/scala/Z3Sort.scala
@@ -10,10 +10,10 @@ sealed class Z3Sort private[z3](val ptr: Long, val context: Z3Context) extends Z
 
   override def toString : String = context.sortToString(this)
 
-  lazy val isBoolSort : Boolean = context.isEqSort(this, context.mkBoolSort)
-  lazy val isIntSort : Boolean = context.isEqSort(this, context.mkIntSort)
-  lazy val isIntSetSort : Boolean = context.isEqSort(this, context.mkSetSort(context.mkIntSort))
-  lazy val isRealSort : Boolean = context.isEqSort(this, context.mkRealSort)
+  lazy val isBoolSort : Boolean = context.isEqSort(this, context.mkBoolSort())
+  lazy val isIntSort : Boolean = context.isEqSort(this, context.mkIntSort())
+  lazy val isIntSetSort : Boolean = context.isEqSort(this, context.mkSetSort(context.mkIntSort()))
+  lazy val isRealSort : Boolean = context.isEqSort(this, context.mkRealSort())
 
   locally {
     context.astQueue.track(this)
diff --git a/src/main/scala/z3/scala/dsl/Trees.scala b/src/main/scala/z3/scala/dsl/Trees.scala
index b787eef..f9a3264 100644
--- a/src/main/scala/z3/scala/dsl/Trees.scala
+++ b/src/main/scala/z3/scala/dsl/Trees.scala
@@ -88,11 +88,11 @@ sealed trait NAryPred[+A >: BottomSort <: TopSort] extends Tree[BoolSort] {
 }
 
 case class BoolConstant(value : Boolean) extends Tree[BoolSort] {
-  private[dsl] def build(z3 : Z3Context) = if(value) z3.mkTrue else z3.mkFalse
+  private[dsl] def build(z3 : Z3Context) = if(value) z3.mkTrue() else z3.mkFalse()
 }
 
 case class IntConstant(value : Int) extends Tree[IntSort] {
-  private[dsl] def build(z3 : Z3Context) = z3.mkInt(value, z3.mkIntSort)
+  private[dsl] def build(z3 : Z3Context) = z3.mkInt(value, z3.mkIntSort())
 }
 
 case class CharConstant(value : Char) extends Tree[BVSort] {
@@ -100,11 +100,11 @@ case class CharConstant(value : Char) extends Tree[BVSort] {
 }
 
 case class BoolVar() extends Tree[BoolSort] {
-  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("C", z3.mkBoolSort)
+  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("C", z3.mkBoolSort())
 }
 
 case class IntVar() extends Tree[IntSort] {
-  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("I", z3.mkIntSort)
+  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("I", z3.mkIntSort())
 }
 
 case class CharVar() extends Tree[BVSort] {
@@ -112,7 +112,7 @@ case class CharVar() extends Tree[BVSort] {
 }
 
 case class IntSetVar() extends Tree[SetSort] {
-  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("IS", z3.mkSetSort(z3.mkIntSort))
+  private[dsl] def build(z3 : Z3Context) = z3.mkFreshConst("IS", z3.mkSetSort(z3.mkIntSort()))
 }
 
 case class Eq[+A >: BottomSort <: TopSort](left : Tree[A], right : Tree[A]) extends BinaryPred[A] {
@@ -380,7 +380,7 @@ case class SetSubset[+A >: BottomSort <: SetSort](left : Tree[A], right : Tree[A
 }
 
 case class EmptyIntSet() extends Tree[SetSort] {
-  private [dsl] def build(z3 : Z3Context) = z3.mkEmptySet(z3.mkIntSort)
+  private [dsl] def build(z3 : Z3Context) = z3.mkEmptySet(z3.mkIntSort())
 }
 
 case class SetAdd[+A >: BottomSort <: TopSort](set : Tree[SetSort], elem : Tree[A]) extends Tree[SetSort] {
diff --git a/src/main/scala/z3/scala/dsl/package.scala b/src/main/scala/z3/scala/dsl/package.scala
index 0ee7eea..6e1fa7b 100644
--- a/src/main/scala/z3/scala/dsl/package.scala
+++ b/src/main/scala/z3/scala/dsl/package.scala
@@ -111,7 +111,7 @@ package object dsl {
   // Predefined ValHandler's
 
   implicit object BooleanValHandler extends ValHandler[Boolean] {
-    def mkSort(z3 : Z3Context) : Z3Sort = z3.mkBoolSort
+    def mkSort(z3 : Z3Context) : Z3Sort = z3.mkBoolSort()
 
     def convert(model : Z3Model, ast : Z3AST) : Boolean =
       model.evalAs[Boolean](ast).getOrElse(false)
@@ -120,7 +120,7 @@ package object dsl {
   }
 
   implicit object IntValHandler extends ValHandler[Int] {
-    def mkSort(z3 : Z3Context) : Z3Sort = z3.mkIntSort
+    def mkSort(z3 : Z3Context) : Z3Sort = z3.mkIntSort()
 
     def convert(model : Z3Model, ast : Z3AST) : Int =
       model.evalAs[Int](ast).getOrElse(0)
@@ -177,20 +177,20 @@ package object dsl {
 
   def find[T:ValHandler](predicate : Val[T] => Tree[BoolSort]) : Option[T] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     val vh = implicitly[ValHandler[T]]
     val value = new Val[T]
     val valAST = value.tree.ast(z3)
     val constraintTree = predicate(value)
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetModel match {
+    solver.checkAndGetModel() match {
       case (Some(true), m) => {
         val result = vh.convert(m, valAST)
-        z3.delete
+        z3.delete()
         Some(result)
       }
       case (_, m) => {
-        z3.delete
+        z3.delete()
         None
       }
     }
@@ -198,14 +198,14 @@ package object dsl {
 
   def findAll[T:ValHandler](predicate : Val[T] => Tree[BoolSort]) : Iterator[T] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     val vh = implicitly[ValHandler[T]]
     val value = new Val[T]
     val valAST = value.tree.ast(z3)
     val constraintTree = predicate(value)
 
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetAllModels.map(m => {
+    solver.checkAndGetAllModels().map(m => {
       val result = vh.convert(m, valAST)
       result
     })
@@ -218,7 +218,7 @@ package object dsl {
 
   def find[T1:ValHandler,T2:ValHandler](predicate : (Val[T1],Val[T2]) => Tree[BoolSort]) : Option[(T1,T2)] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     val vh1 = implicitly[ValHandler[T1]]
     val vh2 = implicitly[ValHandler[T2]]
     val value1 = new Val[T1]
@@ -227,15 +227,15 @@ package object dsl {
     val valAST2 = value2.tree.ast(z3)
     val constraintTree = predicate(value1,value2)
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetModel match {
+    solver.checkAndGetModel() match {
       case (Some(true), m) => {
         val result1 = vh1.convert(m, valAST1)
         val result2 = vh2.convert(m, valAST2)
-        z3.delete
+        z3.delete()
         Some((result1,result2))
       }
       case (_, m) => {
-        z3.delete
+        z3.delete()
         None
       }
     }
@@ -243,7 +243,7 @@ package object dsl {
 
   def findAll[T1:ValHandler,T2:ValHandler](predicate : (Val[T1],Val[T2]) => Tree[BoolSort]) : Iterator[(T1,T2)] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     val vh1 = implicitly[ValHandler[T1]]
     val vh2 = implicitly[ValHandler[T2]]
     val value1 = new Val[T1]
@@ -253,7 +253,7 @@ package object dsl {
     val constraintTree = predicate(value1, value2)
 
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetAllModels.map(m => {
+    solver.checkAndGetAllModels().map(m => {
       val result1 = vh1.convert(m, valAST1)
       val result2 = vh2.convert(m, valAST2)
       (result1,result2)
@@ -267,7 +267,7 @@ package object dsl {
 
   def find[T1:ValHandler,T2:ValHandler,T3:ValHandler](predicate : (Val[T1],Val[T2],Val[T3]) => Tree[BoolSort]) : Option[(T1,T2,T3)] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     val vh1 = implicitly[ValHandler[T1]]
     val vh2 = implicitly[ValHandler[T2]]
     val vh3 = implicitly[ValHandler[T3]]
@@ -279,16 +279,16 @@ package object dsl {
     val valAST3 = value3.tree.ast(z3)
     val constraintTree = predicate(value1,value2, value3)
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetModel match {
+    solver.checkAndGetModel() match {
       case (Some(true), m) => {
         val result1 = vh1.convert(m, valAST1)
         val result2 = vh2.convert(m, valAST2)
         val result3 = vh3.convert(m, valAST3)
-        z3.delete
+        z3.delete()
         Some((result1,result2,result3))
       }
       case (_, m) => {
-        z3.delete
+        z3.delete()
         None
       }
     }
@@ -296,7 +296,7 @@ package object dsl {
 
   def findAll[T1:ValHandler,T2:ValHandler,T3:ValHandler](predicate : (Val[T1],Val[T2],Val[T3]) => Tree[BoolSort]) : Iterator[(T1,T2,T3)] = {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
 
     val vh1 = implicitly[ValHandler[T1]]
     val vh2 = implicitly[ValHandler[T2]]
@@ -310,7 +310,7 @@ package object dsl {
     val constraintTree = predicate(value1, value2, value3)
 
     solver.assertCnstr(constraintTree.ast(z3))
-    solver.checkAndGetAllModels.map(m => {
+    solver.checkAndGetAllModels().map(m => {
       val result1 = vh1.convert(m, valAST1)
       val result2 = vh2.convert(m, valAST2)
       val result3 = vh3.convert(m, valAST3)
diff --git a/src/test/scala/z3/scala/ADTs.scala b/src/test/scala/z3/scala/ADTs.scala
index d65dd3a..56d012a 100644
--- a/src/test/scala/z3/scala/ADTs.scala
+++ b/src/test/scala/z3/scala/ADTs.scala
@@ -7,7 +7,7 @@ class ADTs extends FunSuite with Matchers {
     val ctx = new Z3Context("MODEL" -> true)
 
     toggleWarningMessages(true)
-    val intSort = ctx.mkIntSort
+    val intSort = ctx.mkIntSort()
 
     import Z3Context.{RecursiveType,RegularSort}
 
@@ -83,7 +83,7 @@ class ADTs extends FunSuite with Matchers {
     //// x > 4
     //ctx.assertCnstr(ctx.mkGT(x, ctx.mkInt(4, intSort)))
 
-    val solver = ctx.mkSolver
+    val solver = ctx.mkSolver()
     solver.assertCnstr(t1 === leafCons())
     solver.assertCnstr(nodeValueSelector(t1) === ctx.mkInt(4, intSort))
 
@@ -97,12 +97,12 @@ class ADTs extends FunSuite with Matchers {
 
     //println(ctx.mkImplies(isNode(t2), nodeValueSelector(t2) === ctx.mkInt(12, intSort)))
 
-    val (sol, model) = solver.checkAndGetModel
+    val (sol, model) = solver.checkAndGetModel()
 
     sol should equal(Some(true))
     model.eval(t1) should equal(Some(leafCons()))
 
-    ctx.delete
+    ctx.delete()
   }
 }
 
diff --git a/src/test/scala/z3/scala/Abs.scala b/src/test/scala/z3/scala/Abs.scala
index c33d418..8f73df8 100644
--- a/src/test/scala/z3/scala/Abs.scala
+++ b/src/test/scala/z3/scala/Abs.scala
@@ -7,22 +7,22 @@ class Abs extends FunSuite with Matchers {
   test("array-map absolute value") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val intArraySort = z3.mkArraySort(is, is)
     val array1 = z3.mkFreshConst("arr", intArraySort)
     val array2 = z3.mkFreshConst("arr", intArraySort)
 
     val abs = z3.getAbsFuncDecl()
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
 
     solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(0, is)), z3.mkInt(1, is)))
     solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(1, is)), z3.mkInt(0, is)))
     solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(2, is)), z3.mkInt(-1, is)))
 
     solver.assertCnstr(z3.mkEq(array2, z3.mkArrayMap(abs, array1)))
-    
-    val (result, model) = solver.checkAndGetModel
+
+    val (result, model) = solver.checkAndGetModel()
 
     result should equal(Some(true))
 
@@ -30,7 +30,8 @@ class Abs extends FunSuite with Matchers {
     array2Ev should be (Symbol("defined"))
     val array2Val = model.getArrayValue(array2Ev.get)
     array2Val should be (Symbol("defined"))
-    val (valueMap, default) = array2Val.get
+    val (valueMap0, default) = array2Val.get
+    val valueMap = valueMap0.withDefaultValue(default)
     valueMap(z3.mkInt(0, is)) should equal (z3.mkInt(1, is))
     valueMap(z3.mkInt(1, is)) should equal (z3.mkInt(0, is))
     valueMap(z3.mkInt(2, is)) should equal (z3.mkInt(1, is))
diff --git a/src/test/scala/z3/scala/Arrays.scala b/src/test/scala/z3/scala/Arrays.scala
index 822d3ce..fe1c15b 100644
--- a/src/test/scala/z3/scala/Arrays.scala
+++ b/src/test/scala/z3/scala/Arrays.scala
@@ -7,13 +7,13 @@ class Arrays extends FunSuite with Matchers {
   test("Arrays") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val intArraySort = z3.mkArraySort(is, is)
     val array1 = z3.mkFreshConst("arr", intArraySort)
     val array2 = z3.mkFreshConst("arr", intArraySort)
     val x = z3.mkFreshConst("x", is)
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     // array1 = [ 42, 42, 42, ... ]
     solver.assertCnstr(z3.mkEq(array1,z3.mkConstArray(is, z3.mkInt(42, is))))
     // x = array1[6]
@@ -25,7 +25,7 @@ class Arrays extends FunSuite with Matchers {
     val fourtyTwo = z3.mkFreshConst("ft", is)
     solver.assertCnstr(z3.mkEq(fourtyTwo, z3.mkArrayDefault(array2)))
 
-    val (result, model) = solver.checkAndGetModel
+    val (result, model) = solver.checkAndGetModel()
 
     //println("model is")
     //println(model)
@@ -55,7 +55,7 @@ class Arrays extends FunSuite with Matchers {
         //println("When evaluated, array2 is: " + array2Val)
         array2Val match {
           case Some((valueMap,default)) => {
-            valueMap(z3.mkInt(2, z3.mkIntSort)) should equal (z3.mkInt(0, z3.mkIntSort))
+            valueMap(z3.mkInt(2, z3.mkIntSort())) should equal (z3.mkInt(0, z3.mkIntSort()))
             model.evalAs[Int](default) should equal (Some(42))
           }
           case None =>
diff --git a/src/test/scala/z3/scala/Core.scala b/src/test/scala/z3/scala/Core.scala
index 6726b03..605965e 100644
--- a/src/test/scala/z3/scala/Core.scala
+++ b/src/test/scala/z3/scala/Core.scala
@@ -8,15 +8,15 @@ class Core extends FunSuite with Matchers {
   test("Core") {
     val z3 = new Z3Context("MODEL" -> "true")
 
-    val x = z3.mkFreshConst("x", z3.mkIntSort)
-    val y = z3.mkFreshConst("y", z3.mkIntSort)
-    val p1 = z3.mkFreshConst("p1", z3.mkBoolSort)
-    val p2 = z3.mkFreshConst("p2", z3.mkBoolSort)
-    val p3 = z3.mkFreshConst("p3", z3.mkBoolSort)
-  
-    val zero = z3.mkInt(0, z3.mkIntSort)
-
-    val solver = z3.mkSolver
+    val x = z3.mkFreshConst("x", z3.mkIntSort())
+    val y = z3.mkFreshConst("y", z3.mkIntSort())
+    val p1 = z3.mkFreshConst("p1", z3.mkBoolSort())
+    val p2 = z3.mkFreshConst("p2", z3.mkBoolSort())
+    val p3 = z3.mkFreshConst("p3", z3.mkBoolSort())
+
+    val zero = z3.mkInt(0, z3.mkIntSort())
+
+    val solver = z3.mkSolver()
     solver.assertCnstr(p1 --> !(!(x === zero)))
     solver.assertCnstr(p2 --> !(y === zero))
     solver.assertCnstr(p3 --> !(x === zero))
diff --git a/src/test/scala/z3/scala/IntArith.scala b/src/test/scala/z3/scala/IntArith.scala
index e6c7d2d..6f19387 100644
--- a/src/test/scala/z3/scala/IntArith.scala
+++ b/src/test/scala/z3/scala/IntArith.scala
@@ -6,7 +6,7 @@ class IntArith extends FunSuite with Matchers {
 
   test("Comfusy-like") {
     val z3 = new Z3Context("MODEL" -> true)
-    val i = z3.mkIntSort
+    val i = z3.mkIntSort()
     val h = z3.mkConst(z3.mkStringSymbol("h"), i)
     val m = z3.mkConst(z3.mkStringSymbol("m"), i)
     val s = z3.mkConst(z3.mkStringSymbol("s"), i)
@@ -27,18 +27,18 @@ class IntArith extends FunSuite with Matchers {
     val cs3 = z3.mkAnd(z3.mkGE(m, z), z3.mkLT(m, sx))
     val cs4 = z3.mkAnd(z3.mkGE(s, z), z3.mkLT(s, sx))
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     solver.assertCnstr(z3.mkAnd(cs1, cs2, cs3, cs4))
 
     // attempting to solve the constraints
-    val (sol, model) = solver.checkAndGetModel
+    val (sol, model) = solver.checkAndGetModel()
 
     sol should equal(Some(true))
     model.evalAs[Int](h) should equal(Some(0))
     model.evalAs[Int](m) should equal(Some(20))
     model.evalAs[Int](s) should equal(Some(34))
 
-    z3.delete
+    z3.delete()
   }
 }
 
diff --git a/src/test/scala/z3/scala/NQueens.scala b/src/test/scala/z3/scala/NQueens.scala
index 25364dc..78d0d35 100644
--- a/src/test/scala/z3/scala/NQueens.scala
+++ b/src/test/scala/z3/scala/NQueens.scala
@@ -26,16 +26,16 @@ class NQueens extends FunSuite with Matchers {
            (columns(i) - columns(j) !== j - i))
 
     /* We assert all of the above */
-    val solver = ctx.mkSolver
+    val solver = ctx.mkSolver()
     solver.assertCnstr(diffCnstr)
     boundsCnstr map (solver.assertCnstr(_))
     diagonalsCnstr map (solver.assertCnstr(_))
 
-    val nbModels = solver.checkAndGetAllModels.size
+    val nbModels = solver.checkAndGetAllModels().size
 
     //println("Total number of models: " + nbModels)
     nbModels should equal (92)
 
-    ctx.delete
+    ctx.delete()
   }
 }
diff --git a/src/test/scala/z3/scala/Optimizer.scala b/src/test/scala/z3/scala/Optimizer.scala
index 49e44b4..cb20c64 100644
--- a/src/test/scala/z3/scala/Optimizer.scala
+++ b/src/test/scala/z3/scala/Optimizer.scala
@@ -7,7 +7,7 @@ class Optimizer extends FunSuite with Matchers {
   test("Optimizer") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val x = z3.mkIntConst("x")
     val y = z3.mkIntConst("y")
 
@@ -15,7 +15,7 @@ class Optimizer extends FunSuite with Matchers {
     val a2 = z3.mkLT(x, y)
     val a3 = z3.mkLE(z3.mkAdd(y, x), z3.mkInt(0, is))
 
-    val opt = z3.mkOptimizer
+    val opt = z3.mkOptimizer()
     opt.assertCnstr(z3.mkIff(a3, a1))
     opt.assertCnstr(z3.mkOr(a3, a2))
     opt.assertCnstr(a3,           3)
@@ -23,10 +23,10 @@ class Optimizer extends FunSuite with Matchers {
     opt.assertCnstr(z3.mkNot(a1), 10)
     opt.assertCnstr(z3.mkNot(a2), 3)
 
-    val result = opt.check
+    val result = opt.check()
     result should equal (Some(true))
 
-    val model = opt.getModel
+    val model = opt.getModel()
     val a1eval = model.evalAs[Boolean](a1)
     val a2eval = model.evalAs[Boolean](a2)
     val a3eval = model.evalAs[Boolean](a3)
diff --git a/src/test/scala/z3/scala/Quantifiers.scala b/src/test/scala/z3/scala/Quantifiers.scala
index fe88b93..d61ffed 100644
--- a/src/test/scala/z3/scala/Quantifiers.scala
+++ b/src/test/scala/z3/scala/Quantifiers.scala
@@ -10,16 +10,16 @@ class Quantifiers extends FunSuite with Matchers {
    * (declare-fun array-of (Type) Type)
    * (assert (forall ((x Type)) (subtype x x)))
    * (assert (forall ((x Type) (y Type) (z Type))
-   *             (=> (and (subtype x y) (subtype y z)) 
-   *                             (subtype x z)))) 
+   *             (=> (and (subtype x y) (subtype y z))
+   *                             (subtype x z))))
    * (assert (forall ((x Type) (y Type))
-   *             (=> (and (subtype x y) (subtype y x)) 
+   *             (=> (and (subtype x y) (subtype y x))
    *                             (= x y))))
    * (assert (forall ((x Type) (y Type) (z Type))
-   *             (=> (and (subtype x y) (subtype x z)) 
-   *                             (or (subtype y z) (subtype z y))))) 
+   *             (=> (and (subtype x y) (subtype x z))
+   *                             (or (subtype y z) (subtype z y)))))
    * (assert (forall ((x Type) (y Type))
-   *             (=> (subtype x y) 
+   *             (=> (subtype x y)
    *                             (subtype (array-of x) (array-of y)))))
    * (declare-const root-type Type)
    * (assert (forall ((x Type)) (subtype x root-type)))
@@ -28,7 +28,7 @@ class Quantifiers extends FunSuite with Matchers {
 
   test("Quantifiers") {
     val z3 = new Z3Context("MODEL" -> true)
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
 
     /*
      * (declare-sort Type)
@@ -36,7 +36,7 @@ class Quantifiers extends FunSuite with Matchers {
      * (declare-fun array-of (Type) Type)
      */
     val typeSort = z3.mkUninterpretedSort("Type")
-    val subtype = z3.mkFuncDecl("subtype", List[Z3Sort](typeSort, typeSort).toIndexedSeq, z3.mkBoolSort)
+    val subtype = z3.mkFuncDecl("subtype", List[Z3Sort](typeSort, typeSort).toIndexedSeq, z3.mkBoolSort())
     val arrayOf = z3.mkFuncDecl("array-of", List[Z3Sort](typeSort).toIndexedSeq, typeSort)
 
     val syms @ List(xSym, ySym, zSym) = List("x", "y", "z").map(z3.mkSymbol(_))
@@ -48,28 +48,28 @@ class Quantifiers extends FunSuite with Matchers {
       subtype(x, x)))
 
     /* (assert (forall ((x Type) (y Type) (z Type))
-                   (=> (and (subtype x y) (subtype y z)) 
+                   (=> (and (subtype x y) (subtype y z))
                                   (subtype x z)))) */
     solver.assertCnstr(z3.mkForall(0, Seq.empty,
       Seq(xSym -> typeSort, ySym -> typeSort, zSym -> typeSort),
       z3.mkImplies(z3.mkAnd(subtype(x, y), subtype(y, z)), subtype(x, z))))
 
     /* (assert (forall ((x Type) (y Type))
-                   (=> (and (subtype x y) (subtype y x)) 
+                   (=> (and (subtype x y) (subtype y x))
                                   (= x y)))) */
     solver.assertCnstr(z3.mkForall(0, Seq.empty,
       Seq(xSym -> typeSort, ySym -> typeSort),
       z3.mkImplies(z3.mkAnd(subtype(x, y), subtype(y, x)), z3.mkEq(x, y))))
 
     /* (assert (forall ((x Type) (y Type) (z Type))
-                   (=> (and (subtype x y) (subtype x z)) 
+                   (=> (and (subtype x y) (subtype x z))
                                   (or (subtype y z) (subtype z y))))) */
     solver.assertCnstr(z3.mkForall(0, Seq.empty,
       Seq(xSym -> typeSort, ySym -> typeSort, zSym -> typeSort),
       z3.mkImplies(z3.mkAnd(subtype(x, y), subtype(x, z)), z3.mkOr(subtype(y, z), subtype(z, y)))))
 
     /* (assert (forall ((x Type) (y Type))
-                  (=> (subtype x y) 
+                  (=> (subtype x y)
                                   (subtype (array-of x) (array-of y))))) */
     solver.assertCnstr(z3.mkForall(0, Seq.empty,
       Seq(xSym -> typeSort, ySym -> typeSort),
@@ -83,6 +83,6 @@ class Quantifiers extends FunSuite with Matchers {
       Seq(xSym -> typeSort),
       subtype(x, rootType)))
 
-    solver.check should equal(Some(true))
+    solver.check() should equal(Some(true))
   }
 }
diff --git a/src/test/scala/z3/scala/SatSolver.scala b/src/test/scala/z3/scala/SatSolver.scala
index 9b008ea..d3ba62e 100644
--- a/src/test/scala/z3/scala/SatSolver.scala
+++ b/src/test/scala/z3/scala/SatSolver.scala
@@ -9,7 +9,7 @@ class SatSolver extends FunSuite with Matchers {
     case class Literal(name: String, polarity: Boolean)
     type Clause = Set[Literal]
 
-    def DPLL(f : Set[Clause]) : (Boolean, Map[String,Option[Boolean]]) = 
+    def DPLL(f : Set[Clause]) : (Boolean, Map[String,Option[Boolean]]) =
       if(f.isEmpty) (true, Map.empty)
       else if(f.exists(clause => clause.isEmpty)) (false, Map.empty)
       else {
@@ -19,7 +19,7 @@ class SatSolver extends FunSuite with Matchers {
         val literals = f.reduceLeft((a,b) => a ++ b)
         val litMap: _root_.scala.collection.mutable.Map[String,Z3AST] =
           _root_.scala.collection.mutable.Map.empty[String,Z3AST]
-        
+
         literals.foreach(lit => {
           if(!litMap.keySet.contains(lit.name)) {
             val ast = z3.mkBoolConst(z3.mkStringSymbol(lit.name))
@@ -27,11 +27,11 @@ class SatSolver extends FunSuite with Matchers {
           }
         })
 
-        val solver = z3.mkSolver
+        val solver = z3.mkSolver()
 
         f.foreach(clause => {
           if (clause.size > 1) {
-            val nc: Array[Z3AST] = new Array[Z3AST](clause.size) 
+            val nc: Array[Z3AST] = new Array[Z3AST](clause.size)
             var c: Int = 0
             clause.foreach(lit => {
               nc(c) = if(lit.polarity) litMap(lit.name) else z3.mkNot(litMap(lit.name))
@@ -43,12 +43,12 @@ class SatSolver extends FunSuite with Matchers {
             if(singleLit.polarity)
               solver.assertCnstr(litMap(singleLit.name))
             else
-              solver.assertCnstr(z3.mkNot(litMap(singleLit.name))) 
+              solver.assertCnstr(z3.mkNot(litMap(singleLit.name)))
           }
         })
 
         val (result, model) = solver.checkAndGetModel()
-          
+
         result match {
           case None => println("There was an error with Z3."); (false, Map.empty)
           case Some(false) => (false, Map.empty) // formula was unsat
@@ -65,8 +65,8 @@ class SatSolver extends FunSuite with Matchers {
         val scanner = new _root_.java.util.Scanner(line)
           while(scanner.hasNext) {
           tok = scanner.next
-          if (tok != "0") 
-            {if( tok.startsWith("-")) clause += Literal(tok.drop(1), false) else clause += Literal(tok, true)} 
+          if (tok != "0")
+            {if( tok.startsWith("-")) clause += Literal(tok.drop(1), false) else clause += Literal(tok, true)}
           else {
             form += clause
             clause = Set.empty[Literal]
diff --git a/src/test/scala/z3/scala/Sequences.scala b/src/test/scala/z3/scala/Sequences.scala
index 28b7829..7dda4d7 100644
--- a/src/test/scala/z3/scala/Sequences.scala
+++ b/src/test/scala/z3/scala/Sequences.scala
@@ -7,15 +7,15 @@ class Sequences extends FunSuite with Matchers {
   test("Simple SAT") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val iss = z3.mkSeqSort(is)
     val s1 = z3.mkFreshConst("s1", iss)
     val s2 = z3.mkFreshConst("s2", iss)
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     solver.assertCnstr(z3.mkDistinct(s1, s2))
 
-    val (result, model) = solver.checkAndGetModel
+    val (result, model) = solver.checkAndGetModel()
     result should equal (Some(true))
 
     val s1eval = model.eval(s1)
@@ -28,34 +28,34 @@ class Sequences extends FunSuite with Matchers {
   test("Different head") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val iss = z3.mkSeqSort(is)
     val s1 = z3.mkFreshConst("s1", iss)
     val s2 = z3.mkFreshConst("s2", iss)
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     solver.assertCnstr(z3.mkEq(s1, s2))
     solver.assertCnstr(z3.mkEq(z3.mkUnitSeq(z3.mkInt(1, is)), z3.mkSeqExtract(s1, z3.mkInt(0, is), z3.mkInt(1, is))))
     solver.assertCnstr(z3.mkEq(z3.mkUnitSeq(z3.mkInt(0, is)), z3.mkSeqExtract(s2, z3.mkInt(0, is), z3.mkInt(1, is))))
 
-    val result = solver.check
+    val result = solver.check()
     result should equal (Some(false))
   }
 
   test("Compatible sub-sequences") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val iss = z3.mkSeqSort(is)
     val s1 = z3.mkFreshConst("s1", iss)
     val s2 = z3.mkFreshConst("s2", iss)
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     solver.assertCnstr(z3.mkEq(s1, s2))
     solver.assertCnstr(z3.mkEq(z3.mkUnitSeq(z3.mkInt(1, is)), z3.mkSeqExtract(s1, z3.mkInt(0, is), z3.mkInt(1, is))))
     solver.assertCnstr(z3.mkEq(z3.mkUnitSeq(z3.mkInt(0, is)), z3.mkSeqExtract(s2, z3.mkInt(1, is), z3.mkInt(1, is))))
 
-    val (result, model) = solver.checkAndGetModel
+    val (result, model) = solver.checkAndGetModel()
     result should equal (Some(true))
 
     val s1eval = model.eval(s1)
diff --git a/src/test/scala/z3/scala/Sets.scala b/src/test/scala/z3/scala/Sets.scala
index 2e67905..9a7700d 100644
--- a/src/test/scala/z3/scala/Sets.scala
+++ b/src/test/scala/z3/scala/Sets.scala
@@ -7,15 +7,15 @@ class Sets extends FunSuite with Matchers {
   test("Sets") {
     val z3 = new Z3Context("MODEL" -> true)
 
-    val is = z3.mkIntSort
+    val is = z3.mkIntSort()
     val iss = z3.mkSetSort(is)
     val s1 = z3.mkFreshConst("s1", iss)
     val s2 = z3.mkFreshConst("s2", iss)
 
-    val solver = z3.mkSolver
+    val solver = z3.mkSolver()
     solver.assertCnstr(z3.mkDistinct(s1, s2))
 
-    val (result, model) = solver.checkAndGetModel
+    val (result, model) = solver.checkAndGetModel()
     result should equal(Some(true))
 
     val s1eval = model.eval(s1)
diff --git a/z3_mk_abs.patch b/z3_mk_abs.patch
new file mode 100644
index 0000000..ecd904b
--- /dev/null
+++ b/z3_mk_abs.patch
@@ -0,0 +1,48 @@
+diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp
+index 57f96dd6d..5fe7b8497 100644
+--- a/src/api/api_arith.cpp
++++ b/src/api/api_arith.cpp
+@@ -65,6 +65,7 @@ extern "C" {
+     MK_BINARY_ARITH_OP(Z3_mk_power, OP_POWER);
+     MK_BINARY_ARITH_OP(Z3_mk_mod, OP_MOD);
+     MK_BINARY_ARITH_OP(Z3_mk_rem, OP_REM);
++    MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP);
+ 
+     Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast n1, Z3_ast n2) {
+         Z3_TRY;
+diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
+index d11ce313e..208269021 100644
+--- a/src/api/api_ast.cpp
++++ b/src/api/api_ast.cpp
+@@ -1041,6 +1041,7 @@ extern "C" {
+             case OP_TO_REAL: return Z3_OP_TO_REAL;
+             case OP_TO_INT: return Z3_OP_TO_INT;
+             case OP_IS_INT: return Z3_OP_IS_INT;
++            case OP_ABS: return Z3_OP_ABS;
+             default:
+                 return Z3_OP_INTERNAL;
+             }
+diff --git a/src/api/z3_api.h b/src/api/z3_api.h
+index d5bd1e11c..703301492 100644
+--- a/src/api/z3_api.h
++++ b/src/api/z3_api.h
+@@ -1032,6 +1032,7 @@ typedef enum {
+     Z3_OP_TO_INT,
+     Z3_OP_IS_INT,
+     Z3_OP_POWER,
++    Z3_OP_ABS,
+ 
+     // Arrays & Sets
+     Z3_OP_STORE = 0x300,
+@@ -2420,6 +2421,11 @@ extern "C" {
+     */
+     Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[]);
+ 
++    /**
++       def_API('Z3_mk_abs', AST, (_in(CONTEXT), _in(AST)))
++    */
++    Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast t1);
++
+     /**
+        \brief Create an AST node representing \ccode{args[0] * ... * args[num_args-1]}.
+