From 646c121b6bb98ac07acef6609b6beba4b775cdc8 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Tue, 13 Dec 2022 08:24:32 -0600
Subject: [PATCH] Update versions of external tools

---
 docker/Dockerfile        | 11 +++++------
 lfsc/get-lfsc-checker.sh |  2 +-
 src/flags.ml             |  8 ++++----
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/docker/Dockerfile b/docker/Dockerfile
index ce09c16b8..73613b8b4 100644
--- a/docker/Dockerfile
+++ b/docker/Dockerfile
@@ -21,18 +21,17 @@ RUN eval $(opam env) && \
 FROM alpine:latest
 
 # Retrieve Yices 2
-RUN wget -qq https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz \
- && tar xvf yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz \
- && cp ./yices-2.6.2/bin/yices-smt2 /bin/ \
+RUN wget -qq https://yices.csl.sri.com/releases/2.6.4/yices-2.6.4-x86_64-pc-linux-gnu.tar.gz \
+ && tar xvf yices-2.6.4-x86_64-pc-linux-gnu.tar.gz \
+ && cp ./yices-2.6.4/bin/yices-smt2 /bin/ \
  && rm -rf yices-* \
  && echo Success || true
 
 # Retrieve JKind and cvc5 (required for certification)
-RUN wget -qq https://github.com/loonwerks/jkind/releases/download/v4.4.2/jkind-4.4.2.zip && unzip jkind-4.4.2.zip \
+RUN wget -qq https://github.com/loonwerks/jkind/releases/download/v4.5.2/jkind-4.5.2.zip && unzip jkind-4.5.2.zip \
  && cp ./jkind/jkind ./jkind/*.jar /bin/ \
  && rm -rf jkind* \
- #&& wget -qq https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux -O cvc5 \
- && wget -qq https://github.com/cvc5/cvc5/releases/download/latest/cvc5-Linux-2022-11-17-25e52a4 -O cvc5 \
+ && wget -qq https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux -O cvc5 \
  && mv cvc5 /bin/ \
  && chmod a+x /bin/cvc5 \
  && echo Success || true
diff --git a/lfsc/get-lfsc-checker.sh b/lfsc/get-lfsc-checker.sh
index 7796c06df..f44878488 100755
--- a/lfsc/get-lfsc-checker.sh
+++ b/lfsc/get-lfsc-checker.sh
@@ -35,7 +35,7 @@ make install
 ##### signatures
 
 # The LFSC signatures live in the main cvc5 repository
-version="25e52a430a29c9471ecf772b0bd913417a3be2af"
+version="cvc5-1.0.3"
 SIG_DIR_URL="https://raw.githubusercontent.com/cvc5/cvc5/$version/proofs/lfsc/signatures"
 
 # install signatures and scripts
diff --git a/src/flags.ml b/src/flags.ml
index 3c28dd5ba..0d9e7e42d 100644
--- a/src/flags.ml
+++ b/src/flags.ml
@@ -3565,15 +3565,15 @@ let solver_dependant_actions solver =
           Log.log L_error "Kind 2 requires cvc5 1.0.0 or later. Found version: %d.%d.%d"
             major minor patch ;
           raise Error
-        ) (*;
+        ) ;
         if
-          Certif.proof () && (major = 0 || (major = 1 && minor = 0 && patch < 3))
+          Certif.proof () && not (major=1 && minor=0 && patch=3)
         then (
           Log.log L_error
-            "LFSC proof production requires cvc5 1.0.3 or later. Found \
+            "LFSC proof production requires cvc5 1.0.3. Found \
              version: %d.%d.%d"
             major minor patch;
-          raise Error)*)
+          raise Error)
   )
   | `Yices_native -> (
     let cmd = Format.asprintf "%s --version" (Smt.yices_bin ()) in