diff --git a/.github/workflows/make-tests.yml b/.github/workflows/make-tests.yml
index 53ba54c4a..361e9bc81 100644
--- a/.github/workflows/make-tests.yml
+++ b/.github/workflows/make-tests.yml
@@ -26,6 +26,7 @@ jobs:
       run: |
         make
         make unittests
+        make test testz3 testyices
         make tests
 
   build-win:
@@ -54,7 +55,7 @@ jobs:
           wget,
           unzip,
           python
-    - name: make tests
+    - name: make
       shell: bash
       env:
         CYGWIN: winsymlinks:native
@@ -62,4 +63,11 @@ jobs:
       run: >-
         make &&
         make unittests &&
+        make test testz3 testyices testppl
+    - name: make tests
+      shell: bash
+      env:
+        CYGWIN: winsymlinks:native
+      working-directory: ./prism
+      run: >-
         make tests
diff --git a/CHANGELOG.txt b/CHANGELOG.txt
index c71be33ce..06df781aa 100644
--- a/CHANGELOG.txt
+++ b/CHANGELOG.txt
@@ -71,6 +71,16 @@ Version 1.0 (first released 18/10/2012)
 
 Below are the details of the changes in each new version of PRISM.
 
+-----------------------------------------------------------------------------
+Changes since last release (up to a6d86d21)
+-----------------------------------------------------------------------------
+
+* Updates/fixes in install/launch/testing scripts and build process
+* New -javaversion switch to show Java version used
+* New tests in etc/tests available for easier build tests
+* Transition reward export (MDP-like models) for explicit engine
+* Various bugfixes
+
 -----------------------------------------------------------------------------
 Version 4.8 (first released 5/7/2023)
 -----------------------------------------------------------------------------
diff --git a/prism/Makefile b/prism/Makefile
index d73e8ee67..4f951ba88 100644
--- a/prism/Makefile
+++ b/prism/Makefile
@@ -163,32 +163,6 @@ JAVA_JNI_H_DIR = $(shell \
 JAVA_JNI_MD_H_DIR = $(shell (ls "$(JAVA_JNI_H_DIR)"/jni_md.h "$(JAVA_JNI_H_DIR)"/*/jni_md.h | head -n 1 | sed 's/\/jni_md.h//') 2>/dev/null)
 JAVA_INCLUDES = -I $(JAVA_JNI_H_DIR) -I $(JAVA_JNI_MD_H_DIR)
 
-########
-# PPL  #
-########
-
-# PPL_DIR needs to be set to the location of the Parma Polyhedra Library installation.
-# (More precisely PPL_DIR should contain a directory 'ppl' containing libppl_java.* and ppl_java.jar)
-# This makefile will try to detect this automatically based on the information provided by the ppl-config command.
-# If this detection does not work, or you wish to override it,
-# either set the variable yourself by uncommenting and/or modifying one of the lines below
-# or pass a value to make directly, e.g.: make PPL_DIR=/usr/local/ppl/lib
-
-# Find PPL
-PPL_DIR = $(shell src/scripts/findppl.sh)
-
-#PPL_DIR = 		/usr/local/ppl/lib
-#PPL_DIR = 		/usr/local/lib
-
-# Expected names of (some) PPL files
-ifeq ($(OSTYPE),linux)
-	PPL_JAVA_LIB = libppl_java.so
-endif
-ifeq ($(OSTYPE),darwin)
-	PPL_JAVA_LIB = libppl_java.jnilib
-endif
-PPL_JAVA_JAR = ppl_java.jar
-
 ##################
 # Compilers etc. #
 ##################
@@ -368,7 +342,7 @@ export CFLAGS CXXFLAGS LDFLAGS JFLAGS LIBPREFIX LIBSUFFIX
 
 MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterface pepa/compiler simulator jltl2ba jltl2dstar explicit pta param strat automata common cex
 
-EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices
+EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices ppl
 
 .PHONY: clean javadoc tests release
 
@@ -377,7 +351,7 @@ EXT_PACKAGES = lpsolve55 lp_solve_5.5_java z3 yices
 
 default: all
 
-all: cuddpackage ppl extpackages prism
+all: cuddpackage extpackages prism
 
 # Build our customised version of CUDD
 cuddpackage: checks
@@ -385,34 +359,6 @@ cuddpackage: checks
 	cd $(CUDD_DIR) && \
 	$(MAKE) ICFLAGS="$(DEBUG) $(OPTIMISE) $(WARNINGS)" XCFLAGS="$(filter-out $(DEBUG) $(OPTIMISE) $(WARNINGS),$(CFLAGS))"
 
-# Copy PPL libraries to lib dir
-# (only if not already there, to avoid repeated copying).
-# We check for PPL_JAVA_LIB, which is consistently named
-# and whose presence likely indicates that the files have already been copied.
-# If not found, we use a local copy of the JAR (in ext/ppl_java) since this is needed for compilation.
-ppl: checks
-	@echo Copying PPL files ...; \
-	if [ "$(PPL_DIR)" = "" ]; then \
-		echo "PPL_DIR not specified/detected: cannot copy files"; \
-	else \
-		if [ -f "$(PRISM_LIB_DIR)"/"$(PPL_JAVA_LIB)" ]; then \
-			echo "PPL Java library $(PRISM_LIB_DIR)/$(PPL_JAVA_LIB) detected: nothing to do"; \
-		else \
-			(cp "$(PPL_DIR)"/ppl/"$(PPL_JAVA_LIB)" "$(PRISM_LIB_DIR)" || echo Failed to copy PPL Java library); \
-			(cp "$(PPL_DIR)"/ppl/"$(PPL_JAVA_JAR)" "$(PRISM_LIB_DIR)" || echo Failed to copy PPL Java JAR); \
-			if [ "$(OSTYPE)" = "linux" ]; then \
-				(cp "$(PPL_DIR)"/libppl.so.[0-9][0-9] "$(PRISM_LIB_DIR)" || echo Failed to copy PPL library); \
-			fi; \
-			if [ "$(OSTYPE)" = "darwin" ]; then \
-				(cp "$(PPL_DIR)"/libppl.[0-9][0-9].*lib "$(PRISM_LIB_DIR)" || echo Failed to copy PPL library); \
-			fi; \
-		fi; \
-	fi ; \
-	if [ ! -f "$(PRISM_LIB_DIR)"/"$(PPL_JAVA_JAR)" ]; then \
-		echo "PPL library files not copied; using local copy of JAR"; \
-		cp ext/ppl_java/"$(PPL_JAVA_JAR)" "$(PRISM_LIB_DIR)"; \
-	fi
-
 # Use this to force a rebuild (with javacc) of the main parser
 parser:
 	@echo Making parser ...; \
@@ -525,20 +471,6 @@ checks:
 	  echo "\033[0m"; \
 	  exit 1; \
 	fi; \
-	if [ "$(PPL_DIR)" = "" ]; then \
-	  echo "\033[33mPRISM was unable to find the directory which contains"; \
-	  echo "the Parma Polyhedra Library (PPL). Please specify this "; \
-	  echo "manually to make, as in this example:"; \
-	  echo; \
-	  echo "  make PPL_DIR=/usr/local/ppl/lib"; \
-	  echo; \
-	  echo "See the PRISM manual for further information."; \
-	  echo; \
-	  echo "Alternatively, if you wish, you can set the environment"; \
-	  echo "variable yourself (using setenv or export) or you"; \
-	  echo "can edit the value of PPL_DIR directly in the Makefile."; \
-	  echo "\033[0m"; \
-	fi; \
 	if [ ! -d "$(JAVA_DIR)" ]; then \
 	  echo "\033[33mJava directory \"$(JAVA_DIR)\" does not exist."; \
 	  echo "\033[0m"; \
@@ -562,7 +494,6 @@ checks:
 	echo "JAVA_DIR_BACKUP: $(JAVA_DIR_BACKUP)"; \
 	echo "JAVAC (which): "`which $(JAVAC)`; \
 	echo "JAVAC (version): "$(shell $(JAVAC) -version) \
-	echo "PPL_DIR: $(PPL_DIR)" \
 	)
 
 # Misc: count the number of lines of code
@@ -602,7 +533,7 @@ testyices:
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 tests: testslocal
 	@if [ -d ../prism-tests ]; then \
-	  etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
+	  etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
 	else \
 	  echo "Skipping tests"; \
 	fi
@@ -610,13 +541,13 @@ tests: testslocal
 # Just display the command to run the test suite on this version of PRISM
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 testsecho:
-	@echo etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS)
+	@echo etc/scripts/prism-auto -t -m ../prism-tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS)
 
 # Run local tests (in ./tests)
 # Optionally, extra arguments for prism-auto are picked up via variable TESTS_ARGS
 testslocal:
 	@if [ -d tests ]; then \
-	  etc/scripts/prism-auto -t -m tests -p bin/prism --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
+	  etc/scripts/prism-auto -t -m tests -p bin/prism --print-failures --nailgun --ngprism bin/ngprism $(TESTS_ARGS); \
 	else \
 	  echo "Skipping local tests"; \
 	fi
@@ -629,7 +560,7 @@ testslocal:
 testsfull:
 	etc/scripts/prism-auto -t -m ../prism-tests \
 	--skip-export-runs --skip-duplicate-runs --test-all -a ../prism-tests/all-engines.args --timeout 1m \
-	-p bin/prism --nailgun $(TESTS_ARGS);
+	-p bin/prism --print-failures --nailgun $(TESTS_ARGS);
 
 ##########################
 # Building distributions #
@@ -735,20 +666,16 @@ clean: checks
 celan: clean
 
 # Clean PRISM + CUDD and external libs
-clean_all: checks clean_cudd clean_ppl clean_ext clean clean_tests
+clean_all: checks clean_cudd clean_ext clean clean_tests
 
 clean_cudd:
 	@(cd $(CUDD_DIR) && $(MAKE) distclean)
 
-# Remove PPL libraries copied to lib
-clean_ppl:
-	@rm -f $(PRISM_LIB_DIR)/libppl* $(PRISM_LIB_DIR)/"$(PPL_JAVA_JAR)"
-
 clean_ext:
 	@(for ext in $(EXT_PACKAGES); do \
 	  echo Cleaning $$ext ...; \
 	  (cd ext/$$ext && \
-	  $(MAKE) -s clean) \
+	  $(MAKE) -s OSTYPE="$(OSTYPE)" ARCH="$(ARCH)" clean) \
 	  || exit 1; \
 	done )
 
diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto
index 2fb84ff5b..a48308325 100755
--- a/prism/etc/scripts/prism-auto
+++ b/prism/etc/scripts/prism-auto
@@ -679,8 +679,13 @@ def runPrism(args, bmArgs, dir=""):
             for line in open(logFile, 'r').readlines():
                 if re.match('Error:', line):
                     printTestResult(line)
-            print("To see log file, run:")
-            print("edit " + logFile)
+            if (options.printFailures):
+                print("Failing test log file:")
+                for line in open(logFile, 'r').readlines():
+                    print(line, end="")
+            else:
+                print("To see log file, run:")
+                print("edit " + logFile)
             prismArgsPrint = list(prismArgs)
             prismArgsPrint[0] = options.prismExec
             print("To re-run failing test:")
@@ -1162,6 +1167,7 @@ parser.add_option("--skip-duplicate-runs", action="store_true", dest="skipDuplic
 parser.add_option("--timeout", dest="timeout", metavar="N", default=None, help='Timeout for each PRISM run (examples values for N: 5 / 5s for seconds, 5m / 5h for minutes / hours)')
 parser.add_option("--dd-warnings", action="store_true", dest="ddWarnings", default=False, help="Print the DD reference count warnings")
 parser.add_option("--colour", dest="colourEnabled", metavar="X", type="choice", choices=["yes","no","auto"], default="auto", help="Whether to colour test results: yes, no, auto (yes iff in terminal mode) [default=auto]")
+parser.add_option("--print-failures", action="store_true", dest="printFailures", default=False, help="Display logs for failing tests")
 (options, args) = parser.parse_args()
 if len(args) < 1:
     parser.print_help()
diff --git a/prism/etc/scripts/prism-install-cygwin b/prism/etc/scripts/prism-install-cygwin
index 4caaaf3a2..232462a07 100755
--- a/prism/etc/scripts/prism-install-cygwin
+++ b/prism/etc/scripts/prism-install-cygwin
@@ -12,5 +12,5 @@ git clone https://github.com/prismmodelchecker/prism-games.git
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi
diff --git a/prism/etc/scripts/prism-install-fedora b/prism/etc/scripts/prism-install-fedora
index 15e70a548..dd3d10e5f 100755
--- a/prism/etc/scripts/prism-install-fedora
+++ b/prism/etc/scripts/prism-install-fedora
@@ -19,5 +19,5 @@ git clone https://github.com/prismmodelchecker/prism-games.git
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testppl testyices testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi
diff --git a/prism/etc/scripts/prism-install-ubuntu b/prism/etc/scripts/prism-install-ubuntu
index fd90a3384..a99f8fdcd 100755
--- a/prism/etc/scripts/prism-install-ubuntu
+++ b/prism/etc/scripts/prism-install-ubuntu
@@ -20,55 +20,8 @@ sudo apt -y install python3
 # Download the latest development version from GitHub
 git clone https://github.com/prismmodelchecker/prism-games.git
 
-# Find the Java directory
-export JAVA_HOME=`prism-games/prism/src/scripts/findjavac.sh | sed 's/\/bin\/javac//'`
-
-# Download/build PPL + dependencies (needs Java 8 it seems)
-# Comment out the section below if multi-obj support not needed
-sudo apt -y install openjdk-8-jdk libgmp-dev m4
-export JAVA8_HOME=`find /usr/lib/jvm -name 'java-8*'`
-wget http://www.bugseng.com/products/ppl/download/ftp/releases/1.2/ppl-1.2.tar.gz
-tar xfz ppl-1.2.tar.gz
-cd ppl-1.2
-./configure --enable-interfaces=java --with-java=$JAVA8_HOME
-make
-sudo make install
-cd ..
-
-# Download and build Yices 2.6.2 + Java wrapper
-# Commented out for now since yices binaries are included
-# sudo apt -y install gperf libgmp-dev
-# wget https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-src.tar.gz
-# tar xvfz yices-2.6.2-src.tar.gz
-# cd yices-2.6.2
-# ./configure
-# make
-# sudo make install
-# cp /usr/local/lib/libyices.so.2.6 ../prism-games/prism/ext/yices
-# cd ..
-# git clone https://github.com/SRI-CSL/yices2_java_bindings
-# cd yices2_java_bindings
-# ./ant.sh
-# jar cvfm dist/lib/yices.jar MANIFEST.txt -C build/classes .
-# cp dist/lib/libyices2java.so ../prism-games/prism/ext/yices
-# cp dist/lib/yices.jar ../prism-games/prism/ext/yices
-# cd ..
-
-# Download and build Z3 4.8.7
-# Commented out for now since z3 binaries are included
-# sudo apt -y install python
-# wget https://github.com/Z3Prover/z3/archive/z3-4.8.7.tar.gz
-# tar xvfz z3-4.8.7.tar.gz
-# cd z3-z3-4.8.7
-# python scripts/mk_make.py --java
-# cd build
-# make
-# sudo make install
-# cp /usr/lib/libz3.so ../prism-games/prism/lib
-# cd ..
-
 # Compile PRISM-games and run a few tests (unless --nobuild passed)
 # (should ultimately display: "Testing result: PASS")
 if [ "$*" = "${*/--nobuild}" ]; then
-  (cd prism-games/prism && make && make test testppl testyices testz3)
+  (cd prism-games/prism && make && make test testyices testz3 testppl)
 fi
diff --git a/prism/etc/scripts/prism-install-windows.bat b/prism/etc/scripts/prism-install-windows.bat
index 5a3251ecb..5d88fe60d 100755
--- a/prism/etc/scripts/prism-install-windows.bat
+++ b/prism/etc/scripts/prism-install-windows.bat
@@ -17,3 +17,6 @@ setx PATH "%ProgramFiles(x86)%\NSIS;%PATH%"
 @REM Get and install Cygwin, with core packages needed for PRISM install
 "%SystemRoot%\System32\WindowsPowerShell\v1.0\powershell.exe" -Command "wget -Uri  http://cygwin.com/setup-x86_64.exe -Outfile setup-x86_64.exe
 .\setup-x86_64.exe -P make -P mingw64-x86_64-gcc-g++ -P binutils -P dos2unix -P git -P wget -P unzip -P python -P nano -q -s http://ftp.inf.tu-dresden.de/software/windows/cygwin/
+
+@REM Launch a Cygwin terminal
+"%HOMEDRIVE%\cygwin64\bin\mintty.exe" -
diff --git a/prism/ext/README.md b/prism/ext/README.md
index 3ac7e4990..da4b60cfd 100644
--- a/prism/ext/README.md
+++ b/prism/ext/README.md
@@ -4,6 +4,12 @@ To simplify maintenance of scripts and config files, we mostly omit version numb
 
 * lpsolve (and its Java wrapper) - modification of version 5.5.2.0 (and version 5.5.0.14)
 
+* Z3 (and its Java interface) - version 4.12.4
+
+* Yices 2 (and its Java interface) - version 2.6.4 (and version 1.0.1 ish)
+
+* PPL (and its Java interface) - modification of version 1.2
+
 See here for more details and links:
 
 http://www.prismmodelchecker.org/other-downloads.php
diff --git a/prism/ext/ppl/Makefile b/prism/ext/ppl/Makefile
new file mode 100644
index 000000000..ee4d48470
--- /dev/null
+++ b/prism/ext/ppl/Makefile
@@ -0,0 +1,62 @@
+################################################
+#  NB: This Makefile is designed to be called  #
+#      from the main PRISM Makefile. It won't  #
+#      work on its own because it needs        #
+#      various options to be passed in         #
+################################################
+
+default: all
+
+all: checks libfiles
+
+# Files to copy
+NATIVE_LIBS =
+ifdef OSTYPE
+	NATIVE_LIBS = $(wildcard $(OSTYPE)/$(ARCH)/*)
+endif
+NATIVE_LIBS_COPY = $(NATIVE_LIBS:$(OSTYPE)/$(ARCH)/%=../../$(PRISM_LIB_DIR)/%)
+COMMON_LIBS = $(wildcard common/*)
+COMMON_LIBS_COPY = $(COMMON_LIBS:common/%=../../$(PRISM_LIB_DIR)/%)
+
+# Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
+checks:
+	@if [ "$(LIBSUFFIX)" = "" ]; then \
+	  (echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
+	fi; 
+
+# Copy files/links if they exist and are newer
+# If a file is in both an OS-specific directory and common, the former takes precedence
+
+libfiles: $(NATIVE_LIBS_COPY) $(COMMON_LIBS_COPY)
+	@if [ "$(NATIVE_LIBS_COPY)" = "" ]; then \
+	  echo "Missing pre-built native libraries for $(OSTYPE) $(ARCH)"; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: $(OSTYPE)/$(ARCH)/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: common/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+clean: checks
+	# Remove installed files if present
+	@if [ "$(COMMON_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(COMMON_LIBS_COPY)" && rm -f "$(COMMON_LIBS_COPY)"; \
+	fi
+	@if [ "$(NATIVE_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(NATIVE_LIBS_COPY)" && rm -f "$(NATIVE_LIBS_COPY)"; \
+	fi
+	# Overapproximate and remove all native libraries files for any OS
+	rm -f ../../$(PRISM_LIB_DIR)/*lib*ppl*
+	rm -f ../../$(PRISM_LIB_DIR)/*ppl*dll*
+
+celan:	clean
+
+
+#################################################
diff --git a/prism/ext/ppl/README.md b/prism/ext/ppl/README.md
new file mode 100644
index 000000000..6358dc636
--- /dev/null
+++ b/prism/ext/ppl/README.md
@@ -0,0 +1,152 @@
+This directory contains pre-compiled versions of the Parma Polyhedra Library (PPL) library
+and its Java interface. The Makefile copies the correct versions to the PRISM lib directory.
+
+---
+
+Instructions to build the libraries from source on different OSs are below.
+
+We build GMP from source first. This allows us to statically link GMP
+to the PPL shared libraries, minimising dependencies to bundle.
+Also, we need JNI friendly libraries for Cygwin.
+We use a custom version of PPL that has some build fixes and additions,
+including the option to statically link GMP.
+
+---
+
+### Linux
+
+(assuming set up as in prism-install-ubuntu)
+
+```
+# Pre-requisites
+sudo apt -y install autoconf automake libtool
+
+# Set-up
+export BUILD_DIR="$HOME/tools"
+export JAVA_HOME=/usr/lib/jvm/default-java
+
+# Build a dynamic GMP and a static GMP (incl. C++)
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-cxx --disable-static --enable-shared --prefix=$BUILD_DIR/dynamic_gmp CC=gcc ABI=64 CFLAGS='-fPIC' CPPFLAGS=-DPIC
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-cxx --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp CC=gcc ABI=64 CFLAGS='-fPIC' CPPFLAGS=-DPIC
+make && make install
+# make check
+
+# Build (custom) PPL with Java interface
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/prismmodelchecker/ppl.git
+cd ppl
+autoreconf -i
+./configure --enable-interfaces=java --with-java="$JAVA_HOME" --disable-documentation --prefix=$BUILD_DIR --with-gmp-include="$BUILD_DIR/static_gmp/include" --with-gmp-lib-static="$BUILD_DIR/static_gmp/lib/libgmpxx.a $BUILD_DIR/static_gmp/lib/libgmp.a" CXXFLAGS="-std=c++11" JAVACFLAGS="--release 9"
+make
+make install
+cp $BUILD_DIR/lib/libppl.so.15 $BUILD_DIR/lib/ppl/libppl_java.so $BUILD_DIR/lib/ppl/ppl_java.jar $BUILD_DIR
+```
+
+Files `libppl.so.15`, `libppl_java.so` an `ppl_java.jar` are then in `$BUILD_DIR`.
+
+### macOS
+
+```
+# Pre-requisites
+brew install autoconf automake libtool
+
+# Set-up
+export BUILD_DIR="$HOME/tools/tmp"
+export JAVA_HOME=/opt/homebrew/Cellar/openjdk/20.0.2/libexec/openjdk.jdk/Contents/Home
+
+# Build a dynamic GMP and a static GMP (incl. C++)
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-cxx --disable-static --enable-shared --prefix=$BUILD_DIR/dynamic_gmp CC=gcc ABI=64 CFLAGS='-fPIC -m64' CPPFLAGS=-DPIC
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-cxx --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp CC=gcc ABI=64 CFLAGS='-fPIC -m64' CPPFLAGS=-DPIC
+make && make install
+# make check
+
+# Build (custom) PPL with Java interface
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/prismmodelchecker/ppl.git
+cd ppl
+autoreconf -i
+./configure --enable-interfaces=java --with-java="$JAVA_HOME" --disable-documentation --prefix=$BUILD_DIR --with-gmp-include="$BUILD_DIR/static_gmp/include" --with-gmp-lib-static="$BUILD_DIR/static_gmp/lib/libgmpxx.a $BUILD_DIR/static_gmp/lib/libgmp.a" CXXFLAGS="-std=c++11" JAVACFLAGS="--release 9"
+make
+make install
+cp $BUILD_DIR/lib/libppl.15.dylib $BUILD_DIR/lib/ppl/libppl_java.jnilib $BUILD_DIR/lib/ppl/ppl_java.jar $BUILD_DIR
+```
+
+Files `libppl.15.dylib`, `libppl_java.jnilib` an `ppl_java.jar` are then in `$BUILD_DIR`.
+
+---
+
+### Cygwin
+
+(assuming set up as in prism-install-win.bat/prism-install-cygwin)
+
+```
+# Pre-requisites
+/cygdrive/c/Users/Administrator/setup-x86_64 -P autoconf -P automake -P libtool -q
+
+# Set-up
+export BUILD_DIR="/tools"
+export JAVA_HOME="/cygdrive/c/Program Files/Eclipse Adoptium/jdk-11.0.21.9-hotspot"
+export LIBWINPTHREAD_DIR="/cygdrive/c/cygwin64/usr/x86_64-w64-mingw32/sys-root/mingw/bin"
+
+# Java install without spaces (PPL configure breaks)
+mkdir -p "$BUILD_DIR" && ln -s "$JAVA_HOME" "$BUILD_DIR/java"
+export JAVA_HOME2="$BUILD_DIR/java"
+
+# Build a dynamic GMP and a static GMP (incl. C++)
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx LDFLAGS="-Wl,--add-stdcall-alias" --enable-shared --disable-static --prefix=$BUILD_DIR/dynamic_gmp
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx LDFLAGS="-Wl,--add-stdcall-alias" --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp
+make && make install
+# make check
+
+# Build (custom) PPL with Java interface
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/prismmodelchecker/ppl.git
+cd ppl
+autoreconf -i -f
+# NB: Omit --build=i686-pc-cygwin from configure otherwise jlong test fails
+./configure --host=x86_64-w64-mingw32 --enable-interfaces=java --with-java="$JAVA_HOME2" --disable-documentation --prefix=$BUILD_DIR --with-gmp-include="$BUILD_DIR/static_gmp/include" --with-gmp-lib-static="$BUILD_DIR/static_gmp/lib/libgmpxx.a $BUILD_DIR/static_gmp/lib/libgmp.a" CXXFLAGS="-std=c++11" LDFLAGS="-static-libgcc -static-libstdc++ -Wl,--add-stdcall-alias -Wl,-Bstatic,--whole-archive -lpthread -Wl,-Bdynamic,--no-whole-archive -L$LIBWINPTHREAD_DIR" JAVACFLAGS="--release 9"
+make
+make install
+# Manually rebuild shared libs, letting g++ take care of linking and doing static gcc/c++/lpthread properly
+(cd src && x86_64-w64-mingw32-g++ -shared -static-libgcc -static-libstdc++ -Wl,--add-stdcall-alias -Wl,-Bstatic,--whole-archive -lpthread -Wl,-Bdynamic,--no-whole-archive .libs/assertions.o .libs/Box.o .libs/checked.o .libs/Checked_Number.o .libs/Float.o .libs/fpu-ia32.o .libs/BDS_Status.o .libs/Box_Status.o .libs/Og_Status.o .libs/Concrete_Expression.o .libs/Constraint.o .libs/Constraint_System.o .libs/Congruence.o .libs/Congruence_System.o .libs/Generator_System.o .libs/Grid_Generator_System.o .libs/Generator.o .libs/Grid_Generator.o .libs/Handler.o .libs/Init.o .libs/Coefficient.o .libs/Linear_Expression.o .libs/Linear_Expression_Impl.o .libs/Linear_Expression_Interface.o .libs/Linear_Form.o .libs/Scalar_Products.o .libs/MIP_Problem.o .libs/PIP_Tree.o .libs/PIP_Problem.o .libs/Poly_Con_Relation.o .libs/Poly_Gen_Relation.o .libs/BHRZ03_Certificate.o .libs/H79_Certificate.o .libs/Grid_Certificate.o .libs/Partial_Function.o .libs/Polyhedron_nonpublic.o .libs/Polyhedron_public.o .libs/Polyhedron_chdims.o .libs/Polyhedron_widenings.o .libs/C_Polyhedron.o .libs/NNC_Polyhedron.o .libs/Grid_nonpublic.o .libs/Grid_public.o .libs/Grid_chdims.o .libs/Grid_widenings.o .libs/BD_Shape.o .libs/Octagonal_Shape.o .libs/Pointset_Powerset.o .libs/CO_Tree.o .libs/Sparse_Row.o .libs/Dense_Row.o .libs/Bit_Matrix.o .libs/Bit_Row.o .libs/Ph_Status.o .libs/Grid_Status.o .libs/Variable.o .libs/Variables_Set.o .libs/Grid_conversion.o .libs/Grid_simplify.o .libs/set_GMP_memory_alloc_funcs.o .libs/stdiobuf.o .libs/c_streambuf.o .libs/globals.o .libs/mp_std_bits.o .libs/Weight_Profiler.o .libs/version.o .libs/termination.o .libs/wrap_string.o .libs/Time.o .libs/Watchdog.o .libs/Threshold_Watcher.o $BUILD_DIR/static_gmp/lib/libgmpxx.a $BUILD_DIR/static_gmp/lib/libgmp.a -g -O2 -o .libs/libppl-15.dll -Wl,--enable-auto-image-base -Xlinker --out-implib -Xlinker .libs/libppl.dll.a)
+(cd interfaces/Java/jni && x86_64-w64-mingw32-g++ -shared -static-libgcc -static-libstdc++ -Wl,--add-stdcall-alias -Wl,-Bstatic,--whole-archive -lpthread -Wl,-Bdynamic,--no-whole-archive .libs/ppl_java_common.o .libs/ppl_java_globals.o .libs/ppl_java_Termination.o .libs/ppl_java_Polyhedron.o .libs/ppl_java_Grid.o .libs/ppl_java_Rational_Box.o .libs/ppl_java_BD_Shape_mpz_class.o .libs/ppl_java_BD_Shape_mpq_class.o .libs/ppl_java_Octagonal_Shape_mpz_class.o .libs/ppl_java_Octagonal_Shape_mpq_class.o .libs/ppl_java_Constraints_Product_C_Polyhedron_Grid.o .libs/ppl_java_Pointset_Powerset_C_Polyhedron.o .libs/ppl_java_Pointset_Powerset_NNC_Polyhedron.o .libs/ppl_java_Double_Box.o .libs/ppl_java_BD_Shape_double.o .libs/ppl_java_Octagonal_Shape_double.o ../../../src/.libs/libppl.dll.a $BUILD_DIR/static_gmp/lib/libgmpxx.a $BUILD_DIR/static_gmp/lib/libgmp.a -g -O2 -Wl,--kill-at -o .libs/libppl_java.dll -Wl,--enable-auto-image-base -Xlinker --out-implib -Xlinker .libs/libppl_java.dll.a)
+make install
+cp $BUILD_DIR/bin/libppl-15.dll $BUILD_DIR
+cp $BUILD_DIR/lib/ppl/libppl_java.dll $BUILD_DIR/ppl_java.dll
+cp $BUILD_DIR/lib/ppl/ppl_java.jar $BUILD_DIR
+```
+
+Files `libppl-15.dll`, `ppl_java.dll` an `ppl_java.jar` are then in `$BUILD_DIR`.
diff --git a/prism/ext/ppl/common/ppl_java.jar b/prism/ext/ppl/common/ppl_java.jar
new file mode 100644
index 000000000..9eb96df4b
Binary files /dev/null and b/prism/ext/ppl/common/ppl_java.jar differ
diff --git a/prism/ext/ppl/cygwin/x86_64/libppl-15.dll b/prism/ext/ppl/cygwin/x86_64/libppl-15.dll
new file mode 100755
index 000000000..db7306c58
Binary files /dev/null and b/prism/ext/ppl/cygwin/x86_64/libppl-15.dll differ
diff --git a/prism/ext/ppl/cygwin/x86_64/libppl.dll b/prism/ext/ppl/cygwin/x86_64/libppl.dll
new file mode 120000
index 000000000..089d56be5
--- /dev/null
+++ b/prism/ext/ppl/cygwin/x86_64/libppl.dll
@@ -0,0 +1 @@
+libppl-15.dll
\ No newline at end of file
diff --git a/prism/ext/ppl/cygwin/x86_64/ppl_java.dll b/prism/ext/ppl/cygwin/x86_64/ppl_java.dll
new file mode 100755
index 000000000..8131be0f9
Binary files /dev/null and b/prism/ext/ppl/cygwin/x86_64/ppl_java.dll differ
diff --git a/prism/ext/ppl/darwin/arm64/libppl.15.dylib b/prism/ext/ppl/darwin/arm64/libppl.15.dylib
new file mode 100755
index 000000000..4556c20c3
Binary files /dev/null and b/prism/ext/ppl/darwin/arm64/libppl.15.dylib differ
diff --git a/prism/ext/ppl/darwin/arm64/libppl.dylib b/prism/ext/ppl/darwin/arm64/libppl.dylib
new file mode 120000
index 000000000..0d97e76de
--- /dev/null
+++ b/prism/ext/ppl/darwin/arm64/libppl.dylib
@@ -0,0 +1 @@
+libppl.15.dylib
\ No newline at end of file
diff --git a/prism/ext/ppl/darwin/arm64/libppl_java.jnilib b/prism/ext/ppl/darwin/arm64/libppl_java.jnilib
new file mode 100755
index 000000000..8fca087aa
Binary files /dev/null and b/prism/ext/ppl/darwin/arm64/libppl_java.jnilib differ
diff --git a/prism/ext/ppl/darwin/x86_64/libppl.15.dylib b/prism/ext/ppl/darwin/x86_64/libppl.15.dylib
new file mode 100755
index 000000000..d968d77cf
Binary files /dev/null and b/prism/ext/ppl/darwin/x86_64/libppl.15.dylib differ
diff --git a/prism/ext/ppl/darwin/x86_64/libppl.dylib b/prism/ext/ppl/darwin/x86_64/libppl.dylib
new file mode 120000
index 000000000..0d97e76de
--- /dev/null
+++ b/prism/ext/ppl/darwin/x86_64/libppl.dylib
@@ -0,0 +1 @@
+libppl.15.dylib
\ No newline at end of file
diff --git a/prism/ext/ppl/darwin/x86_64/libppl_java.jnilib b/prism/ext/ppl/darwin/x86_64/libppl_java.jnilib
new file mode 100755
index 000000000..2ce2a8cfa
Binary files /dev/null and b/prism/ext/ppl/darwin/x86_64/libppl_java.jnilib differ
diff --git a/prism/ext/ppl/linux/aarch64/libppl.so b/prism/ext/ppl/linux/aarch64/libppl.so
new file mode 120000
index 000000000..c768c105e
--- /dev/null
+++ b/prism/ext/ppl/linux/aarch64/libppl.so
@@ -0,0 +1 @@
+libppl.so.15
\ No newline at end of file
diff --git a/prism/ext/ppl/linux/aarch64/libppl.so.15 b/prism/ext/ppl/linux/aarch64/libppl.so.15
new file mode 100755
index 000000000..a5cb9c3a2
Binary files /dev/null and b/prism/ext/ppl/linux/aarch64/libppl.so.15 differ
diff --git a/prism/ext/ppl/linux/aarch64/libppl_java.so b/prism/ext/ppl/linux/aarch64/libppl_java.so
new file mode 100755
index 000000000..6caf065b6
Binary files /dev/null and b/prism/ext/ppl/linux/aarch64/libppl_java.so differ
diff --git a/prism/ext/ppl/linux/amd64/libppl.so b/prism/ext/ppl/linux/amd64/libppl.so
new file mode 120000
index 000000000..c768c105e
--- /dev/null
+++ b/prism/ext/ppl/linux/amd64/libppl.so
@@ -0,0 +1 @@
+libppl.so.15
\ No newline at end of file
diff --git a/prism/ext/z3/libz3.so b/prism/ext/ppl/linux/amd64/libppl.so.15
similarity index 66%
rename from prism/ext/z3/libz3.so
rename to prism/ext/ppl/linux/amd64/libppl.so.15
index b6fd53475..a57dc9f8e 100755
Binary files a/prism/ext/z3/libz3.so and b/prism/ext/ppl/linux/amd64/libppl.so.15 differ
diff --git a/prism/ext/ppl/linux/amd64/libppl_java.so b/prism/ext/ppl/linux/amd64/libppl_java.so
new file mode 100755
index 000000000..7d3803a86
Binary files /dev/null and b/prism/ext/ppl/linux/amd64/libppl_java.so differ
diff --git a/prism/ext/ppl_java/ppl_java.jar b/prism/ext/ppl_java/ppl_java.jar
deleted file mode 100644
index 2f73d96a6..000000000
Binary files a/prism/ext/ppl_java/ppl_java.jar and /dev/null differ
diff --git a/prism/ext/yices/Makefile b/prism/ext/yices/Makefile
index 51640e41e..960d52304 100644
--- a/prism/ext/yices/Makefile
+++ b/prism/ext/yices/Makefile
@@ -7,20 +7,16 @@
 
 default: all
 
-all: checks yices
-
-# MacOS libs
-ifeq ($(OSTYPE),darwin)
-    YICES_LIB = $(LIBPREFIX)yices.2$(LIBSUFFIX)
-    YICES_JAVA_LIB = $(LIBPREFIX)yices2java$(LIBSUFFIX)
-    GMP_LIB = $(LIBPREFIX)gmp.10$(LIBSUFFIX)
-# Anything else (including unsupported OSs) - Linux libs
-else
-    YICES_LIB = $(LIBPREFIX)yices$(LIBSUFFIX).2.6
-    YICES_JAVA_LIB = $(LIBPREFIX)yices2java$(LIBSUFFIX)
-    GMP_LIB = $(LIBPREFIX)gmp$(LIBSUFFIX).10
+all: checks libfiles
+
+# Files to copy
+NATIVE_LIBS =
+ifdef OSTYPE
+	NATIVE_LIBS = $(wildcard $(OSTYPE)/$(ARCH)/*)
 endif
-YICES_JAVA_JAR = yices.jar
+NATIVE_LIBS_COPY = $(NATIVE_LIBS:$(OSTYPE)/$(ARCH)/%=../../$(PRISM_LIB_DIR)/%)
+COMMON_LIBS = $(wildcard common/*)
+COMMON_LIBS_COPY = $(COMMON_LIBS:common/%=../../$(PRISM_LIB_DIR)/%)
 
 # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
 checks:
@@ -28,22 +24,37 @@ checks:
 	  (echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
 	fi; 
 
-yices:
-	@(if [ "$(OSTYPE)" = "linux" ]; then \
-	  echo "Copying Yices libraries for Linux"; \
-	  cp "$(YICES_LIB)" "$(YICES_JAVA_LIB)" "$(YICES_JAVA_JAR)" "$(GMP_LIB)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
-	@(if [ "$(OSTYPE)" = "darwin" ]; then \
-	  echo "Copying Yices libraries for MacOS"; \
-	  cp "$(YICES_LIB)" "$(YICES_JAVA_LIB)" "$(YICES_JAVA_JAR)" "$(GMP_LIB)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
-	@(if [ "$(OSTYPE)" = "cygwin" ]; then \
-	  echo "No support for Yices on Windows/Cywgin currently"; \
-	  cp "$(YICES_JAVA_JAR)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
+# Copy files/links if they exist and are newer
+# If a file is in both an OS-specific directory and common, the former takes precedence
+
+libfiles: $(NATIVE_LIBS_COPY) $(COMMON_LIBS_COPY)
+	@if [ "$(NATIVE_LIBS_COPY)" = "" ]; then \
+	  echo "Missing pre-built native libraries for $(OSTYPE) $(ARCH)"; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: $(OSTYPE)/$(ARCH)/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: common/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
 
 clean: checks
-	rm -f "../../$(PRISM_LIB_DIR)/$(YICES_LIB)" "../../$(PRISM_LIB_DIR)/$(YICES_JAVA_LIB)" "../../$(PRISM_LIB_DIR)/$(YICES_JAVA_JAR)"
+	# Remove installed files if present
+	@if [ "$(COMMON_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(COMMON_LIBS_COPY)" && rm -f "$(COMMON_LIBS_COPY)"; \
+	fi
+	@if [ "$(NATIVE_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(NATIVE_LIBS_COPY)" && rm -f "$(NATIVE_LIBS_COPY)"; \
+	fi
+	# Overapproximate and remove all native libraries files for any OS
+	rm -f ../../$(PRISM_LIB_DIR)/*lib*yices*
+	rm -f ../../$(PRISM_LIB_DIR)/*yice*dll*
 
 celan:	clean
 
diff --git a/prism/ext/yices/README.md b/prism/ext/yices/README.md
new file mode 100644
index 000000000..e1bbc9ff7
--- /dev/null
+++ b/prism/ext/yices/README.md
@@ -0,0 +1,191 @@
+This directory contains pre-compiled versions of Yices 2 and its Java interface.
+The Makefile copies the correct versions to the PRISM lib directory.
+
+---
+
+Instructions to build the libraries from source on different OSs are below.
+
+We build GMP and Yices 2 from source. This allows us to statically link GMP
+to the Yices 2 Java wrapper (and to Yices), minimising dependencies to bundle.
+Also, we need PIC libraries for macOS, and JNI friendly libraries for Cygwin.
+
+For GMP and Yices 2, see also:
+
+* [Yices 2 compilation instructions](https://github.com/SRI-CSL/yices2/blob/master/doc/COMPILING)
+* [Yices 2 GMP compilation instructions](https://github.com/SRI-CSL/yices2/blob/master/doc/GMP)
+* [Yices 2 Windows build code](https://github.com/SRI-CSL/yices2/blob/master/.github/workflows/windows_ci.yml)
+
+For the Java wrapper, we don't use the provided scripts since they don't work
+for Cygwin and don't reliably produce jars (and we need extra flags).
+
+---
+
+### Linux
+
+(assuming set up as in prism-install-ubuntu)
+
+```
+# Pre-requisites
+sudo apt -y install autoconf automake libtool gperf
+
+# Set-up
+export BUILD_DIR="$HOME/tools"
+export JAVA_HOME=/usr/lib/jvm/default-java
+
+# Build a dynamic GMP and a static GMP
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --disable-static --enable-shared --prefix=$BUILD_DIR/dynamic_gmp CC=gcc ABI=64 CFLAGS='-fPIC' CPPFLAGS=-DPIC
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp CC=gcc ABI=64 CFLAGS='-fPIC' CPPFLAGS=-DPIC
+make && make install
+# make check
+
+# Build Yices 2
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+wget https://yices.csl.sri.com/releases/2.6.4/yices-2.6.4-src.tar.gz
+tar xfz yices-2.6.4-src.tar.gz
+cd yices2-Yices-2.6.4
+autoconf
+./configure CPPFLAGS=-I$BUILD_DIR/static_gmp/include LDFLAGS=-L$BUILD_DIR/static_gmp/lib --with-pic-gmp=$BUILD_DIR/static_gmp/lib/libgmp.a --with-pic-gmp-include-dir=$BUILD_DIR/static_gmp/include
+make MODE=release static-dist
+cp build/*/static_dist/lib/libyices.so.2.6.4 $BUILD_DIR
+ln -s $BUILD_DIR/libyices.so.2.6.4 $BUILD_DIR/libyices.so.2.6
+ln -s $BUILD_DIR/libyices.so.2.6 $BUILD_DIR/libyices.so.2
+ln -s $BUILD_DIR/libyices.so.2 $BUILD_DIR/libyices.so
+cp build/*/static_dist/include/* $BUILD_DIR
+
+# Build Yices Java bindings
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/SRI-CSL/yices2_java_bindings
+cd yices2_java_bindings
+cd src/main/java/com/sri/yices
+javac --release 9 -d ../../../../../../dist/lib -h . *.java
+g++ -fPIC -I"$JAVA_HOME/include" -I"$JAVA_HOME/include/linux" -I$BUILD_DIR -I$BUILD_DIR/static_gmp/include -c yicesJNI.cpp
+g++ -shared -o libyices2java.so yicesJNI.o $BUILD_DIR/static_gmp/lib/libgmp.a -L$BUILD_DIR -lyices
+cd ../../../../../..
+jar cvfm yices.jar MANIFEST.txt -C dist/lib .
+cp src/main/java/com/sri/yices/libyices2java.so yices.jar $BUILD_DIR
+```
+
+Files `libyices.so.2.6`, `libyices2java.so` and `yices.jar` are then in `$BUILD_DIR`.
+
+### macOS
+
+```
+# Pre-requisites
+brew install autoconf automake libtool gperf
+
+# Set-up
+export BUILD_DIR="$HOME/tools/tmp"
+export JAVA_HOME=/opt/homebrew/Cellar/openjdk/20.0.2/libexec/openjdk.jdk/Contents/Home
+
+# Build a dynamic GMP and a static GMP
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --disable-static --enable-shared --prefix=$BUILD_DIR/dynamic_gmp CC=gcc ABI=64 CFLAGS='-fPIC -m64' CPPFLAGS=-DPIC
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp CC=gcc ABI=64 CFLAGS='-fPIC -m64' CPPFLAGS=-DPIC
+make && make install
+# make check
+
+# Build Yices 2
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+wget https://yices.csl.sri.com/releases/2.6.4/yices-2.6.4-src.tar.gz
+tar xfz yices-2.6.4-src.tar.gz
+cd yices2-Yices-2.6.4
+autoconf
+./configure CPPFLAGS=-I$BUILD_DIR/static_gmp/include LDFLAGS=-L$BUILD_DIR/static_gmp/lib --with-pic-gmp=$BUILD_DIR/static_gmp/lib/libgmp.a --with-pic-gmp-include-dir=$BUILD_DIR/static_gmp/include
+make OPTION=64bits MODE=release static-dist
+cp build/*/static_dist/lib/libyices.2.dylib $BUILD_DIR
+ln -s $BUILD_DIR/libyices.2.dylib $BUILD_DIR/libyices.dylib
+cp build/*/static_dist/include/* $BUILD_DIR
+
+# Build Yices Java bindings
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/SRI-CSL/yices2_java_bindings
+cd yices2_java_bindings
+cd src/main/java/com/sri/yices
+javac --release 9 -d ../../../../../../dist/lib -h . *.java
+g++ -fPIC -I"$JAVA_HOME/include" -I"$JAVA_HOME/include/darwin" -I$BUILD_DIR -I$BUILD_DIR/static_gmp/include -c yicesJNI.cpp
+g++ -dynamiclib -o libyices2java.dylib yicesJNI.o $BUILD_DIR/static_gmp/lib/libgmp.a -L$BUILD_DIR -lyices
+cd ../../../../../..
+jar cvfm yices.jar MANIFEST.txt -C dist/lib .
+cp src/main/java/com/sri/yices/libyices2java.dylib yices.jar $BUILD_DIR
+```
+
+Files `libyices.2.dylib`, `libyices2java.dylib` and `yices.jar` are then in `$BUILD_DIR`.
+
+---
+
+### Cygwin
+
+(assuming set up as in prism-install-win.bat/prism-install-cygwin)
+
+```
+# Pre-requisites
+/cygdrive/c/Users/Administrator/setup-x86_64 -P autoconf -P automake -P libtool -P gperf -q
+
+# Set-up
+export BUILD_DIR="/tools"
+export JAVA_HOME="/cygdrive/c/Program Files/Eclipse Adoptium/jdk-11.0.21.9-hotspot"
+
+# Build a dynamic GMP and a static GMP
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin LDFLAGS="-Wl,--add-stdcall-alias" --enable-shared --disable-static --prefix=$BUILD_DIR/dynamic_gmp
+make && make install
+# make check
+mkdir -p $BUILD_DIR && cd $BUILD_DIR && mkdir -p dynamic_gmp && mkdir -p static_gmp
+rm -rf gmp-6*
+wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
+tar xf gmp-6.3.0.tar.xz
+cd gmp-6.3.0
+./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin LDFLAGS="-Wl,--add-stdcall-alias" --enable-static --disable-shared --prefix=$BUILD_DIR/static_gmp
+make && make install
+# make check
+
+# Build Yices 2
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+wget https://yices.csl.sri.com/releases/2.6.4/yices-2.6.4-src.tar.gz
+tar xfz yices-2.6.4-src.tar.gz
+cd yices2-Yices-2.6.4
+autoconf
+./configure --host=x86_64-w64-mingw32 CPPFLAGS=-I$BUILD_DIR/dynamic_gmp/include LDFLAGS="-L$BUILD_DIR/dynamic_gmp/lib -Wl,--add-stdcall-alias" --with-static-gmp=$BUILD_DIR/static_gmp/lib/libgmp.a --with-static-gmp-include-dir=$BUILD_DIR/static_gmp/include
+export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
+make OPTION=mingw64 MODE=release static-dist
+cp build/*/static_dist/bin/libyices.dll $BUILD_DIR
+cp build/*/static_dist/include/* $BUILD_DIR
+
+# Build Yices Java bindings
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+git clone https://github.com/SRI-CSL/yices2_java_bindings
+cd yices2_java_bindings
+cd src/main/java/com/sri/yices
+javac --release 9 -d ../../../../../../dist/lib -h . *.java
+x86_64-w64-mingw32-g++ -I$JAVA_HOME/include -I$JAVA_HOME/include/win32 -I$BUILD_DIR -I$BUILD_DIR/static_gmp/include -fpermissive -c yicesJNIforWindows.cpp
+x86_64-w64-mingw32-g++ -shared -static-libgcc -static-libstdc++ -Wl,--add-stdcall-alias -Wl,-Bstatic,--whole-archive -lpthread -Wl,-Bdynamic,--no-whole-archive -o yices2java.dll yicesJNIforWindows.o $BUILD_DIR/static_gmp/lib/libgmp.a -L$BUILD_DIR -lyices
+cd ../../../../../..
+jar cvfm yices.jar MANIFEST.txt -C dist/lib .
+cp src/main/java/com/sri/yices/yices2java.dll yices.jar $BUILD_DIR
+```
+
+Files `libyices.dll`, `yices2java.dll` and `yices.jar` are then in `$BUILD_DIR`.
diff --git a/prism/ext/yices/common/yices.jar b/prism/ext/yices/common/yices.jar
new file mode 100644
index 000000000..27f001ffe
Binary files /dev/null and b/prism/ext/yices/common/yices.jar differ
diff --git a/prism/ext/yices/cygwin/x86_64/libyices.dll b/prism/ext/yices/cygwin/x86_64/libyices.dll
new file mode 100755
index 000000000..9dcfc33a8
Binary files /dev/null and b/prism/ext/yices/cygwin/x86_64/libyices.dll differ
diff --git a/prism/ext/yices/cygwin/x86_64/yices2java.dll b/prism/ext/yices/cygwin/x86_64/yices2java.dll
new file mode 100755
index 000000000..1504db02e
Binary files /dev/null and b/prism/ext/yices/cygwin/x86_64/yices2java.dll differ
diff --git a/prism/ext/yices/darwin/arm64/libyices.2.dylib b/prism/ext/yices/darwin/arm64/libyices.2.dylib
new file mode 100755
index 000000000..f689745cf
Binary files /dev/null and b/prism/ext/yices/darwin/arm64/libyices.2.dylib differ
diff --git a/prism/ext/yices/darwin/arm64/libyices.dylib b/prism/ext/yices/darwin/arm64/libyices.dylib
new file mode 120000
index 000000000..c60a38df0
--- /dev/null
+++ b/prism/ext/yices/darwin/arm64/libyices.dylib
@@ -0,0 +1 @@
+libyices.2.dylib
\ No newline at end of file
diff --git a/prism/ext/yices/darwin/arm64/libyices2java.dylib b/prism/ext/yices/darwin/arm64/libyices2java.dylib
new file mode 100755
index 000000000..9d696a771
Binary files /dev/null and b/prism/ext/yices/darwin/arm64/libyices2java.dylib differ
diff --git a/prism/ext/yices/darwin/x86_64/libyices.2.dylib b/prism/ext/yices/darwin/x86_64/libyices.2.dylib
new file mode 100755
index 000000000..001ee29de
Binary files /dev/null and b/prism/ext/yices/darwin/x86_64/libyices.2.dylib differ
diff --git a/prism/ext/yices/darwin/x86_64/libyices.dylib b/prism/ext/yices/darwin/x86_64/libyices.dylib
new file mode 120000
index 000000000..c60a38df0
--- /dev/null
+++ b/prism/ext/yices/darwin/x86_64/libyices.dylib
@@ -0,0 +1 @@
+libyices.2.dylib
\ No newline at end of file
diff --git a/prism/ext/yices/darwin/x86_64/libyices2java.dylib b/prism/ext/yices/darwin/x86_64/libyices2java.dylib
new file mode 100755
index 000000000..605ac6686
Binary files /dev/null and b/prism/ext/yices/darwin/x86_64/libyices2java.dylib differ
diff --git a/prism/ext/yices/libgmp.10.dylib b/prism/ext/yices/libgmp.10.dylib
deleted file mode 100644
index dd04b5871..000000000
Binary files a/prism/ext/yices/libgmp.10.dylib and /dev/null differ
diff --git a/prism/ext/yices/libgmp.so.10 b/prism/ext/yices/libgmp.so.10
deleted file mode 100644
index 5543fcaf3..000000000
Binary files a/prism/ext/yices/libgmp.so.10 and /dev/null differ
diff --git a/prism/ext/yices/libyices.2.dylib b/prism/ext/yices/libyices.2.dylib
deleted file mode 100755
index fd572a1f3..000000000
Binary files a/prism/ext/yices/libyices.2.dylib and /dev/null differ
diff --git a/prism/ext/yices/libyices.so.2.6 b/prism/ext/yices/libyices.so.2.6
deleted file mode 100755
index 7143fe36d..000000000
Binary files a/prism/ext/yices/libyices.so.2.6 and /dev/null differ
diff --git a/prism/ext/yices/libyices2java.dylib b/prism/ext/yices/libyices2java.dylib
deleted file mode 100755
index a90ef1761..000000000
Binary files a/prism/ext/yices/libyices2java.dylib and /dev/null differ
diff --git a/prism/ext/yices/libyices2java.so b/prism/ext/yices/libyices2java.so
deleted file mode 100755
index 44dc4e19a..000000000
Binary files a/prism/ext/yices/libyices2java.so and /dev/null differ
diff --git a/prism/ext/yices/linux/aarch64/libyices.so b/prism/ext/yices/linux/aarch64/libyices.so
new file mode 120000
index 000000000..083b3166c
--- /dev/null
+++ b/prism/ext/yices/linux/aarch64/libyices.so
@@ -0,0 +1 @@
+libyices.so.2
\ No newline at end of file
diff --git a/prism/ext/yices/linux/aarch64/libyices.so.2 b/prism/ext/yices/linux/aarch64/libyices.so.2
new file mode 120000
index 000000000..35f862740
--- /dev/null
+++ b/prism/ext/yices/linux/aarch64/libyices.so.2
@@ -0,0 +1 @@
+libyices.so.2.6
\ No newline at end of file
diff --git a/prism/ext/yices/linux/aarch64/libyices.so.2.6 b/prism/ext/yices/linux/aarch64/libyices.so.2.6
new file mode 120000
index 000000000..4a28862c5
--- /dev/null
+++ b/prism/ext/yices/linux/aarch64/libyices.so.2.6
@@ -0,0 +1 @@
+libyices.so.2.6.4
\ No newline at end of file
diff --git a/prism/ext/yices/linux/aarch64/libyices.so.2.6.4 b/prism/ext/yices/linux/aarch64/libyices.so.2.6.4
new file mode 100755
index 000000000..ba52daf10
Binary files /dev/null and b/prism/ext/yices/linux/aarch64/libyices.so.2.6.4 differ
diff --git a/prism/ext/yices/linux/aarch64/libyices2java.so b/prism/ext/yices/linux/aarch64/libyices2java.so
new file mode 100755
index 000000000..86f930f24
Binary files /dev/null and b/prism/ext/yices/linux/aarch64/libyices2java.so differ
diff --git a/prism/ext/yices/linux/amd64/libyices.so b/prism/ext/yices/linux/amd64/libyices.so
new file mode 120000
index 000000000..083b3166c
--- /dev/null
+++ b/prism/ext/yices/linux/amd64/libyices.so
@@ -0,0 +1 @@
+libyices.so.2
\ No newline at end of file
diff --git a/prism/ext/yices/linux/amd64/libyices.so.2 b/prism/ext/yices/linux/amd64/libyices.so.2
new file mode 120000
index 000000000..35f862740
--- /dev/null
+++ b/prism/ext/yices/linux/amd64/libyices.so.2
@@ -0,0 +1 @@
+libyices.so.2.6
\ No newline at end of file
diff --git a/prism/ext/yices/linux/amd64/libyices.so.2.6 b/prism/ext/yices/linux/amd64/libyices.so.2.6
new file mode 100755
index 000000000..d4cf347c0
Binary files /dev/null and b/prism/ext/yices/linux/amd64/libyices.so.2.6 differ
diff --git a/prism/ext/yices/linux/amd64/libyices2java.so b/prism/ext/yices/linux/amd64/libyices2java.so
new file mode 100755
index 000000000..a3cfadf07
Binary files /dev/null and b/prism/ext/yices/linux/amd64/libyices2java.so differ
diff --git a/prism/ext/yices/yices.jar b/prism/ext/yices/yices.jar
deleted file mode 100644
index 810eae201..000000000
Binary files a/prism/ext/yices/yices.jar and /dev/null differ
diff --git a/prism/ext/z3/Makefile b/prism/ext/z3/Makefile
index d3d8a024d..8d604e859 100644
--- a/prism/ext/z3/Makefile
+++ b/prism/ext/z3/Makefile
@@ -7,18 +7,16 @@
 
 default: all
 
-all: checks z3
-
-# Cygwin libs
-ifeq ($(OSTYPE),cygwin)
-    Z3_LIB = $(LIBPREFIX)libz3$(LIBSUFFIX)
-    Z3_JAVA_LIB = $(LIBPREFIX)libz3java$(LIBSUFFIX)
-# Anything else (including unsupported OSs) - Mac/Linux libs
-else
-    Z3_LIB = $(LIBPREFIX)z3$(LIBSUFFIX)
-    Z3_JAVA_LIB = $(LIBPREFIX)z3java$(LIBSUFFIX)
+all: checks libfiles
+
+# Files to copy
+NATIVE_LIBS =
+ifdef OSTYPE
+	NATIVE_LIBS = $(wildcard $(OSTYPE)/$(ARCH)/*)
 endif
-Z3_JAVA_JAR = com.microsoft.z3.jar
+NATIVE_LIBS_COPY = $(NATIVE_LIBS:$(OSTYPE)/$(ARCH)/%=../../$(PRISM_LIB_DIR)/%)
+COMMON_LIBS = $(wildcard common/*)
+COMMON_LIBS_COPY = $(COMMON_LIBS:common/%=../../$(PRISM_LIB_DIR)/%)
 
 # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
 checks:
@@ -26,22 +24,37 @@ checks:
 	  (echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
 	fi; 
 
-z3:
-	@(if [ "$(OSTYPE)" = "linux" ]; then \
-	  echo "Copying Z3 libraries for Linux"; \
-	  cp "$(Z3_LIB)" "$(Z3_JAVA_LIB)" "$(Z3_JAVA_JAR)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
-	@(if [ "$(OSTYPE)" = "darwin" ]; then \
-	  echo "Copying Z3 libraries for MacOS"; \
-	  cp "$(OSTYPE)/$(ARCH)/$(Z3_LIB)" "$(OSTYPE)/$(ARCH)/$(Z3_JAVA_LIB)" "$(Z3_JAVA_JAR)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
-	@(if [ "$(OSTYPE)" = "cygwin" ]; then \
-	  echo "Copying Z3 libraries for Cywgin"; \
-	  cp "$(Z3_LIB)" "$(Z3_JAVA_LIB)" "$(Z3_JAVA_JAR)" ../../$(PRISM_LIB_DIR)/ ; \
-	fi)
+# Copy files/links if they exist and are newer
+# If a file is in both an OS-specific directory and common, the former takes precedence
+
+libfiles: $(NATIVE_LIBS_COPY) $(COMMON_LIBS_COPY)
+	@if [ "$(NATIVE_LIBS_COPY)" = "" ]; then \
+	  echo "Missing pre-built native libraries for $(OSTYPE) $(ARCH)"; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: $(OSTYPE)/$(ARCH)/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
+
+../../$(PRISM_LIB_DIR)/%: common/%
+	@if [ -f "$<" ]; then \
+	  echo cp -R $< $@; \
+	  cp -R $< $@; \
+	fi
 
 clean: checks
-	rm -f "../../$(PRISM_LIB_DIR)/$(Z3_LIB)" "../../$(PRISM_LIB_DIR)/$(Z3_JAVA_LIB)" "../../$(PRISM_LIB_DIR)/$(Z3_JAVA_JAR)"
+	# Remove installed files if present
+	@if [ "$(COMMON_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(COMMON_LIBS_COPY)" && rm -f "$(COMMON_LIBS_COPY)"; \
+	fi
+	@if [ "$(NATIVE_LIBS_COPY)" != "" ]; then \
+	  echo Removing "$(NATIVE_LIBS_COPY)" && rm -f "$(NATIVE_LIBS_COPY)"; \
+	fi
+	# Overapproximate and remove all native libraries files for any OS
+	rm -f ../../$(PRISM_LIB_DIR)/*lib*z3*
+	rm -f ../../$(PRISM_LIB_DIR)/*z3*dll*
 
 celan:	clean
 
diff --git a/prism/ext/z3/README.md b/prism/ext/z3/README.md
new file mode 100644
index 000000000..315336bda
--- /dev/null
+++ b/prism/ext/z3/README.md
@@ -0,0 +1,38 @@
+This directory contains pre-compiled versions of Z3 and its Java interface.
+The Makefile copies the correct versions to the PRISM lib directory.
+
+---
+
+For macOS/Windows, we take files directly from the Z3 binary releases at
+
+https://github.com/Z3Prover/z3/releases
+
+For Linux, we build from source (instructions below)
+
+* libz3.{so,dylib,dll}
+* libz3java.{so,dylib,dll}
+* com.microsoft.z3.jar
+
+---
+
+### Linux
+
+(assuming set up as in prism-install-ubuntu)
+
+```
+# Set-up
+export BUILD_DIR="$HOME/tools"
+
+# Build Z3 (with Java wrapper)
+mkdir -p $BUILD_DIR && cd $BUILD_DIR
+wget https://github.com/Z3Prover/z3/archive/z3-4.12.4.tar.gz
+tar xvfz z3-4.12.4.tar.gz
+cd z3-z3-4.12.4
+python3 scripts/mk_make.py --java
+cd build
+make
+#sudo make install
+cp libz3.so libz3java.so com.microsoft.z3.jar $BUILD_DIR
+```
+
+Files `libz3.so`, `libz3java.so` and `com.microsoft.z3.jar` are then in `$BUILD_DIR`.
diff --git a/prism/ext/z3/com.microsoft.z3.jar b/prism/ext/z3/com.microsoft.z3.jar
deleted file mode 100644
index 2f4825e33..000000000
Binary files a/prism/ext/z3/com.microsoft.z3.jar and /dev/null differ
diff --git a/prism/ext/z3/common/com.microsoft.z3.jar b/prism/ext/z3/common/com.microsoft.z3.jar
new file mode 100644
index 000000000..2c20912f0
Binary files /dev/null and b/prism/ext/z3/common/com.microsoft.z3.jar differ
diff --git a/prism/ext/z3/libz3.dll b/prism/ext/z3/cygwin/x86_64/libz3.dll
similarity index 59%
rename from prism/ext/z3/libz3.dll
rename to prism/ext/z3/cygwin/x86_64/libz3.dll
index e5c8fc5cb..250eecd70 100755
Binary files a/prism/ext/z3/libz3.dll and b/prism/ext/z3/cygwin/x86_64/libz3.dll differ
diff --git a/prism/ext/z3/cygwin/x86_64/libz3java.dll b/prism/ext/z3/cygwin/x86_64/libz3java.dll
new file mode 100755
index 000000000..6591eef34
Binary files /dev/null and b/prism/ext/z3/cygwin/x86_64/libz3java.dll differ
diff --git a/prism/ext/z3/darwin/arm64/libz3.dylib b/prism/ext/z3/darwin/arm64/libz3.dylib
index d93112ddb..c93d25b90 100755
Binary files a/prism/ext/z3/darwin/arm64/libz3.dylib and b/prism/ext/z3/darwin/arm64/libz3.dylib differ
diff --git a/prism/ext/z3/darwin/arm64/libz3java.dylib b/prism/ext/z3/darwin/arm64/libz3java.dylib
index fe6b7304f..fb5a34251 100755
Binary files a/prism/ext/z3/darwin/arm64/libz3java.dylib and b/prism/ext/z3/darwin/arm64/libz3java.dylib differ
diff --git a/prism/ext/z3/darwin/x86_64/libz3.dylib b/prism/ext/z3/darwin/x86_64/libz3.dylib
index 42db39cb9..caf8b0be8 100755
Binary files a/prism/ext/z3/darwin/x86_64/libz3.dylib and b/prism/ext/z3/darwin/x86_64/libz3.dylib differ
diff --git a/prism/ext/z3/darwin/x86_64/libz3java.dylib b/prism/ext/z3/darwin/x86_64/libz3java.dylib
index a7f41ad68..5218fe18d 100755
Binary files a/prism/ext/z3/darwin/x86_64/libz3java.dylib and b/prism/ext/z3/darwin/x86_64/libz3java.dylib differ
diff --git a/prism/ext/z3/libz3java.dll b/prism/ext/z3/libz3java.dll
deleted file mode 100755
index 1080b4c3a..000000000
Binary files a/prism/ext/z3/libz3java.dll and /dev/null differ
diff --git a/prism/ext/z3/libz3java.so b/prism/ext/z3/libz3java.so
deleted file mode 100755
index 1652e09d9..000000000
Binary files a/prism/ext/z3/libz3java.so and /dev/null differ
diff --git a/prism/ext/z3/linux/aarch64/libz3.so b/prism/ext/z3/linux/aarch64/libz3.so
new file mode 100755
index 000000000..7d53c2a95
Binary files /dev/null and b/prism/ext/z3/linux/aarch64/libz3.so differ
diff --git a/prism/ext/z3/linux/aarch64/libz3java.so b/prism/ext/z3/linux/aarch64/libz3java.so
new file mode 100755
index 000000000..9626130c8
Binary files /dev/null and b/prism/ext/z3/linux/aarch64/libz3java.so differ
diff --git a/prism/ext/z3/linux/amd64/libz3.so b/prism/ext/z3/linux/amd64/libz3.so
new file mode 100755
index 000000000..ae5ee05b7
Binary files /dev/null and b/prism/ext/z3/linux/amd64/libz3.so differ
diff --git a/prism/ext/z3/linux/amd64/libz3java.so b/prism/ext/z3/linux/amd64/libz3java.so
new file mode 100755
index 000000000..0fefc0ba6
Binary files /dev/null and b/prism/ext/z3/linux/amd64/libz3java.so differ