Merge remote-tracking branch 'origin/cvc5' into equiv

bin/build.sh

@@ -25,7 +25,7 @@
 INSTALL_DEPENDENCIES=${INSTALL_DEPENDENCIES:-1}
 INSTALL_MONO=${INSTALL_MONO:-0} # Mono is needed only for lockpwn and symbooglix
 INSTALL_Z3=${INSTALL_Z3:-1}
-INSTALL_CVC4=${INSTALL_CVC4:-0}
+INSTALL_CVC5=${INSTALL_CVC5:-0}
 INSTALL_YICES2=${INSTALL_YICES2:-0}
 INSTALL_BOOGIE=${INSTALL_BOOGIE:-1}
 INSTALL_CORRAL=${INSTALL_CORRAL:-1}
@@ -49,7 +49,7 @@ SMACK_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && cd .. && pwd )"
 ROOT_DIR="$( cd "${SMACK_DIR}" && cd .. && pwd )"
 DEPS_DIR="${ROOT_DIR}/smack-deps"
 Z3_DIR="${DEPS_DIR}/z3"
-CVC4_DIR="${DEPS_DIR}/cvc4"
+CVC5_DIR="${DEPS_DIR}/cvc5"
 YICES2_DIR="${DEPS_DIR}/yices2"
 BOOGIE_DIR="${DEPS_DIR}/boogie"
 CORRAL_DIR="${DEPS_DIR}/corral"
@@ -414,17 +414,17 @@ if [ ${INSTALL_Z3} -eq 1 ] ; then
 fi
 
 
-if [ ${INSTALL_CVC4} -eq 1 ] ; then
-  if [ ! -d "$CVC4_DIR" ] ; then
-    puts "Installing CVC4"
-    mkdir -p ${CVC4_DIR}
-    ${WGET} https://github.com/CVC4/CVC4/releases/download/${CVC4_VERSION}/cvc4-${CVC4_VERSION}-x86_64-linux-opt -O ${CVC4_DIR}/cvc4
-    chmod +x ${CVC4_DIR}/cvc4
-    puts "Installed CVC4"
+if [ ${INSTALL_CVC5} -eq 1 ] ; then
+  if [ ! -d "$CVC5_DIR" ] ; then
+    puts "Installing CVC5"
+    mkdir -p ${CVC5_DIR}
+    ${WGET} https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux -O ${CVC5_DIR}/cvc5
+    chmod +x ${CVC5_DIR}/cvc5
+    puts "Installed CVC5"
   else
-    puts "CVC4 already installed"
+    puts "CVC5 already installed"
   fi
-  echo export PATH=\"${CVC4_DIR}:\$PATH\" >> ${SMACKENV}
+  echo export PATH=\"${CVC5_DIR}:\$PATH\" >> ${SMACKENV}
 fi
 
 

bin/versions

@@ -1,5 +1,5 @@
 Z3_VERSION="4.8.12"
-CVC4_VERSION="1.8"
+CVC5_VERSION="1.0.5"
 YICES2_VERSION="2.6.2"
 BOOGIE_VERSION="2.9.6"
 CORRAL_VERSION="1.1.8"

share/smack/top.py

@@ -546,7 +546,7 @@ def arguments():
         help='back-end verification engine')
 
     verifier_group.add_argument('--solver',
-                                choices=['z3', 'cvc4', "yices2"], default='z3',
+                                choices=['z3', 'cvc5', "yices2"], default='z3',
                                 help='back-end SMT solver')
 
     verifier_group.add_argument(
@@ -942,8 +942,8 @@ def boogie_command(args):
     command += ["/errorLimit:%s" % args.max_violations]
     if not args.modular:
         command += ["/loopUnroll:%d" % args.unroll]
-    if args.solver == 'cvc4':
-        command += ["/proverOpt:SOLVER=cvc4"]
+    if args.solver == 'cvc5':
+        command += ["/proverOpt:SOLVER=CVC5"]
     elif args.solver == 'yices2':
         command += ["/proverOpt:SOLVER=Yices2"]
     return command
@@ -959,8 +959,8 @@ def corral_command(args):
     command += ["/cex:%s" % args.max_violations]
     command += ["/maxStaticLoopBound:%d" % args.loop_limit]
     command += ["/recursionBound:%d" % args.unroll]
-    if args.solver == 'cvc4':
-        command += ["/bopt:proverOpt:SOLVER=cvc4"]
+    if args.solver == 'cvc5':
+        command += ["/bopt:proverOpt:SOLVER=CVC5"]
     elif args.solver == 'yices2':
         command += ["/bopt:proverOpt:SOLVER=Yices2"]
     return command