Update CI, minor fixes (#238)

- updates CI settings and scripts to those from epfl-lara/scala-smtlib
- cross-tests on JDK 17 and 21
- fixes Eldarica version (from nightly) since a new release is now available
- updates scala-smtlib to Scala 3.7 base
- fixes a compilation warning about pattern match exhaustivity

Author: sankalpgambhir

.github/workflows/inox-CI.yml

@@ -9,11 +9,19 @@ jobs:
   tests:
     if: github.event.pull_request.draft == false
     runs-on: [self-hosted, linux]
+    strategy:
+      matrix:
+        java-version: [17, 21]
     env:
       # define Java options for both official sbt and sbt-extras
       JAVA_OPTS_TMP_DIR: ./tmp_java
       JAVA_OPTS: -Xss64M -Xms1024M -Xmx8G -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR
       JVM_OPTS:  -Xss64M -Xms1024M -Xmx8G -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR
+      # solver versions to test against
+      INSTALL_SOLVERS: 1
+      Z3_VER: 4.15.1
+      CVC4_VER: 1.8
+      CVC5_VER: 1.2.1
     steps:
     - name: Checkout
       uses: actions/checkout@v4
@@ -23,16 +31,15 @@ jobs:
       uses: actions/setup-java@v4
       with:
         distribution: temurin
-        java-version: 17
+        java-version: ${{ matrix.java-version }}
     - name: Install and unpack sbt
       run: |
-        wget https://github.com/sbt/sbt/releases/download/v1.10.1/sbt-1.10.1.tgz
-        tar xfz sbt-1.10.1.tgz
+        ./scripts/install_sbt.sh
         echo "PATH=./sbt/bin/:$PATH" >> "$GITHUB_ENV"
     - name: Prepare temp folder
       run: rm -rf $JAVA_OPTS_TMP_DIR && mkdir -p $JAVA_OPTS_TMP_DIR
     - name: Install solvers
-      run: ./install_solvers.sh $GITHUB_WORKSPACE/.local/bin
+      run: ./scripts/install_solvers.sh $GITHUB_WORKSPACE/.local/bin $Z3_VER $CVC4_VER $CVC5_VER
     - name: Add solvers to PATH
       run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
     - name: Test solvers availability

build.sbt

@@ -40,7 +40,7 @@ resolvers ++= Seq(
 libraryDependencies ++= Seq(
   "org.scalatest" %% "scalatest" % "3.2.9" % "test;it",
   "org.apache.commons" % "commons-lang3" % "3.4",
-  ("uuverifiers" %% "eldarica" % "nightly-SNAPSHOT").cross(CrossVersion.for3Use2_13),
+  ("uuverifiers" %% "eldarica" % "2.2").cross(CrossVersion.for3Use2_13),
   ("uuverifiers" %% "princess" % "2025-04-01").cross(CrossVersion.for3Use2_13),
   "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
 )
@@ -67,7 +67,7 @@ lazy val nTestParallelism = {
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val smtlib = RootProject(file("../scala-smtlib")) // If you have a local copy of Scala-SMTLIB and would like to do some changes
-lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "39745509132b01dc3291112c5259f5e77492d42c")
+lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "358d3f1c2d323fcd574cc869ce1d2e6b4f14609c")
 
 lazy val scriptName = settingKey[String]("Name of the generated 'inox' script")
 

install_solvers.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env sh
+
+SBT_VER="$(grep 'sbt.version' project/build.properties | cut -d= -f2)"
+if [ -z "$SBT_VER" ]; then
+  echo "sbt.version not found in project/build.properties"
+  exit 1
+fi
+wget -c https://github.com/sbt/sbt/releases/download/v${SBT_VER}/sbt-${SBT_VER}.tgz -q
+tar xfz "sbt-${SBT_VER}.tgz"

scripts/install_sbt.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env sh
+
+if [ "$INSTALL_SOLVERS" != "1" ]; then
+  echo "Skipping solver installation"
+  exit 0
+fi
+
+TEMP_DIR="$(pwd)/temp"
+SOLVERS_DIR=${1:-"$(pwd)/solvers"}
+
+# check for set version or default to known working (for script) versions
+Z3_VER=${2:-"4.15.1"}
+CVC4_VER=${3:-"1.8"}
+CVC5_VER=${4:-"1.2.1"}
+
+ARCH=$(uname -m)
+# short arch name as used by z3 builds
+SHORT_ARCH=$(uname -m | sed 's/x86_64/x64/;s/aarch64/arm64/;')
+
+# libc linked against z3
+# (glibc for Linux, osx for macOS)
+LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+
+mkdir -p "$SOLVERS_DIR"
+mkdir -p "$TEMP_DIR"
+# cvc5
+wget -c "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-Linux-${ARCH}-static.zip" -O "$TEMP_DIR/cvc5.zip" -q
+unzip "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR" 
+CVC5_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*cvc5*")
+mv "$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5"
+chmod +x "$SOLVERS_DIR/cvc5"
+rm -rf "$TEMP_DIR"
+
+# # CVC4
+wget -c "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" -O "$SOLVERS_DIR/cvc4" -q
+chmod +x "$SOLVERS_DIR/cvc4"
+
+# z3
+mkdir -p "$TEMP_DIR"
+Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
+Z3_URL=$(
+  curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
+  grep "browser_download_url.*${Z3_FILE_PREFIX}" | #| # find url for the correct build
+  sed 's/^.*: //;s/^"//;s/"$//' # strip non-url
+)
+wget -c "${Z3_URL}" -O "$TEMP_DIR/z3.zip" -q
+unzip "$TEMP_DIR/z3.zip" -d "$TEMP_DIR" 
+Z3_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*z3*")
+mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
+chmod +x "$SOLVERS_DIR/z3"
+rm -rf "$TEMP_DIR"
+
+echo "************** Solvers Installed **************"
+exit 0

scripts/install_solvers.sh

@@ -183,6 +183,9 @@ trait TypeElaborators { self: Elaborators =>
           val u = Unknown.fresh
           vds.combine(getExpr(pred, u)(using newStore))({
             case (Seq(vd), pred) => trees.RefinementType(vd, pred)
+            case (vds, _) => 
+              // there were 0 or > 1 bindings, should not happen
+              throw new ElaborationException(Seq(ErrorLocation(s"Invalid refinement type elaboration, expected 1 binding, found ${vds.length}", expr.pos)))
           }).addConstraint({
             Constraint.equal(u, trees.BooleanType())
           })