Update versions of external tools

kind2-mc · Dec 13, 2022 · 646c121 · 646c121
1 parent 0f6bc52
commit 646c121
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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