Merge branch 'master' into splitEqRew

88 files changed, 1309 insertions, 24 deletions

diff --git a/contrib/run-script-casc24-fnt b/contrib/competitions/casc/run-script-casc24-fnt
index b10d7324a..b10d7324a 100755
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/competitions/casc/run-script-casc24-fnt
diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/competitions/casc/run-script-casc24-fnt-no-models
index 3b4d5e320..3b4d5e320 100755
--- a/contrib/run-script-casc24-fnt-no-models
+++ b/contrib/competitions/casc/run-script-casc24-fnt-no-models
diff --git a/contrib/run-script-casc24-fof b/contrib/competitions/casc/run-script-casc24-fof
index b3ede0dfa..b3ede0dfa 100755
--- a/contrib/run-script-casc24-fof
+++ b/contrib/competitions/casc/run-script-casc24-fof
diff --git a/contrib/run-script-casc25-fnt b/contrib/competitions/casc/run-script-casc25-fnt
index 7f007186c..7f007186c 100755
--- a/contrib/run-script-casc25-fnt
+++ b/contrib/competitions/casc/run-script-casc25-fnt
diff --git a/contrib/run-script-casc25-fof b/contrib/competitions/casc/run-script-casc25-fof
index 26c544062..26c544062 100755
--- a/contrib/run-script-casc25-fof
+++ b/contrib/competitions/casc/run-script-casc25-fof
diff --git a/contrib/run-script-casc25-tfa b/contrib/competitions/casc/run-script-casc25-tfa
index 40ed76df5..40ed76df5 100755
--- a/contrib/run-script-casc25-tfa
+++ b/contrib/competitions/casc/run-script-casc25-tfa
diff --git a/contrib/run-script-casc25-tfn b/contrib/competitions/casc/run-script-casc25-tfn
index 6888d7b49..6888d7b49 100755
--- a/contrib/run-script-casc25-tfn
+++ b/contrib/competitions/casc/run-script-casc25-tfn
diff --git a/contrib/run-script-casc26-fnt b/contrib/competitions/casc/run-script-casc26-fnt
index c89d3eb0a..c89d3eb0a 100644
--- a/contrib/run-script-casc26-fnt
+++ b/contrib/competitions/casc/run-script-casc26-fnt
diff --git a/contrib/run-script-casc26-fof b/contrib/competitions/casc/run-script-casc26-fof
index 5ec312cb7..5ec312cb7 100644
--- a/contrib/run-script-casc26-fof
+++ b/contrib/competitions/casc/run-script-casc26-fof
diff --git a/contrib/run-script-casc26-tfa b/contrib/competitions/casc/run-script-casc26-tfa
index 74147e529..74147e529 100644
--- a/contrib/run-script-casc26-tfa
+++ b/contrib/competitions/casc/run-script-casc26-tfa
diff --git a/contrib/competitions/casc/run-script-casc27-fnt b/contrib/competitions/casc/run-script-casc27-fnt
new file mode 100755
index 000000000..301b03a2b
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-fnt
@@ -0,0 +1,35 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference
+finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-fof b/contrib/competitions/casc/run-script-casc27-fof
new file mode 100755
index 000000000..c95266367
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-fof
@@ -0,0 +1,50 @@
+#!/bin/bash
+
+# script is used for FOF division, also SLD division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 20 --no-e-matching --full-saturate-quant
+trywith 15 --finite-model-find --uf-ss=no-minimal
+trywith 5 --multi-trigger-when-single --full-saturate-quant
+trywith 5 --trigger-sel=max --full-saturate-quant
+trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+trywith 10 --multi-trigger-cache --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --fs-interleave --decision=internal --full-saturate-quant
+trywith 15 --relevant-triggers --full-saturate-quant
+trywith 15 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --pre-skolem-quant --full-saturate-quant
+trywith 30 --qcf-vo-exp --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant
+finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-tfa b/contrib/competitions/casc/run-script-casc27-tfa
new file mode 100755
index 000000000..ec4c76685
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-tfa
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+trywith 15 --finite-model-find --decision=internal
+trywith 15 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+trywith 15 --no-e-matching --full-saturate-quant
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant
+finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-tfn-nr b/contrib/competitions/casc/run-script-casc27-tfn-nr
new file mode 100644
index 000000000..b20b68cf9
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-tfn-nr
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfn casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --decision=internal --sort-inference --macros-quant --macros-quant-mode=all
+trywith 15 --nl-ext-tplanes --full-saturate-quant --macros-quant --macros-quant-mode=all
+finishwith --finite-model-find --fmf-inst-engine --sort-inference --macros-quant --macros-quant-mode=all
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-thf b/contrib/competitions/casc/run-script-casc27-thf
new file mode 100755
index 000000000..5db5527ed
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-thf
@@ -0,0 +1,44 @@
+#!/bin/bash
+
+# script is used for THF division
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-thf casc 27 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 20 --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant
+trywith 20 --uf-ho --ho-elim --full-saturate-quant
+trywith 5  --uf-ho --ho-elim --finite-model-find --uf-ss=no-minimal
+trywith 5  --uf-ho --no-ho-matching --finite-model-find --uf-ss=no-minimal
+trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --fs-interleave --ho-elim-store-ax
+trywith 20 --uf-ho --no-ho-matching --full-saturate-quant --macros-quant-mode=all
+trywith 30 --uf-ho --ho-elim --full-saturate-quant --fs-interleave
+trywith 30 --uf-ho --no-ho-matching --full-saturate-quant --ho-elim-store-ax
+finishwith  --uf-ho --ho-elim --no-ho-elim-store-ax --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/competitions/casc/run-script-casc27-thf-sat-nr b/contrib/competitions/casc/run-script-casc27-thf-sat-nr
new file mode 100644
index 000000000..92a1537f9
--- /dev/null
+++ b/contrib/competitions/casc/run-script-casc27-thf-sat-nr
@@ -0,0 +1,35 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-thf casc 27 for SAT : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 2 --uf-ho --finite-model-find --ho-elim
+finishwith --uf-ho --finite-model-find
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj7-fnt b/contrib/competitions/casc/run-script-cascj7-fnt
index e3ad1a2ff..e3ad1a2ff 100755
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/competitions/casc/run-script-cascj7-fnt
diff --git a/contrib/run-script-cascj7-fof b/contrib/competitions/casc/run-script-cascj7-fof
index fb2ca33eb..fb2ca33eb 100755
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/competitions/casc/run-script-cascj7-fof
diff --git a/contrib/run-script-cascj7-tff b/contrib/competitions/casc/run-script-cascj7-tff
index 11350cd7e..11350cd7e 100755
--- a/contrib/run-script-cascj7-tff
+++ b/contrib/competitions/casc/run-script-cascj7-tff
diff --git a/contrib/run-script-cascj8-fnt b/contrib/competitions/casc/run-script-cascj8-fnt
index bc37180a6..bc37180a6 100755
--- a/contrib/run-script-cascj8-fnt
+++ b/contrib/competitions/casc/run-script-cascj8-fnt
diff --git a/contrib/run-script-cascj8-fof b/contrib/competitions/casc/run-script-cascj8-fof
index fe18c3ed0..fe18c3ed0 100755
--- a/contrib/run-script-cascj8-fof
+++ b/contrib/competitions/casc/run-script-cascj8-fof
diff --git a/contrib/run-script-cascj8-tfa b/contrib/competitions/casc/run-script-cascj8-tfa
index da4056466..da4056466 100755
--- a/contrib/run-script-cascj8-tfa
+++ b/contrib/competitions/casc/run-script-cascj8-tfa
diff --git a/contrib/run-script-cascj8-tfn b/contrib/competitions/casc/run-script-cascj8-tfn
index a6fe1e23c..a6fe1e23c 100755
--- a/contrib/run-script-cascj8-tfn
+++ b/contrib/competitions/casc/run-script-cascj8-tfn
diff --git a/contrib/run-script-cascj9-fnt b/contrib/competitions/casc/run-script-cascj9-fnt
index 4e52e8e91..4e52e8e91 100755
--- a/contrib/run-script-cascj9-fnt
+++ b/contrib/competitions/casc/run-script-cascj9-fnt
diff --git a/contrib/run-script-cascj9-fof b/contrib/competitions/casc/run-script-cascj9-fof
index 71107775a..71107775a 100755
--- a/contrib/run-script-cascj9-fof
+++ b/contrib/competitions/casc/run-script-cascj9-fof
diff --git a/contrib/run-script-cascj9-tfa b/contrib/competitions/casc/run-script-cascj9-tfa
index d730db922..d730db922 100755
--- a/contrib/run-script-cascj9-tfa
+++ b/contrib/competitions/casc/run-script-cascj9-tfa
diff --git a/contrib/run-script-cascj9-tfn-nr b/contrib/competitions/casc/run-script-cascj9-tfn-nr
index 8124fd6f9..8124fd6f9 100644
--- a/contrib/run-script-cascj9-tfn-nr
+++ b/contrib/competitions/casc/run-script-cascj9-tfn-nr
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
new file mode 100755
index 000000000..a8c6b0ba4
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -0,0 +1,162 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in which
+# case this run script terminates immediately.  Otherwise, this function
+# returns normally and prints the output of the solver to stderr.
+function trywith {
+  limit=$1; shift;
+  result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+    *)         echo "$result" >&2;;
+  esac
+}
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_LRA)
+  trywith 400 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
+  ;;
+QF_LIA)
+  # same as QF_LRA but add --pb-rewrites
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
+  ;;
+QF_NIA)
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 60 --nl-ext-tplanes --decision=justification
+  trywith 60 --no-nl-ext-tplanes --decision=internal
+  # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
+  trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  finishwith --nl-ext-tplanes --decision=internal
+  ;;
+QF_NRA)
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 600 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 60 --nl-ext-tplanes --decision=internal --solve-real-as-int
+  finishwith --nl-ext-tplanes --decision=justification
+  ;;
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA)
+  # the following is designed for a run time of 20 min.
+  # initial runs 2min
+  trywith 60 --simplification=none --full-saturate-quant
+  trywith 60 --no-e-matching --full-saturate-quant
+  # trigger selections 6min
+  trywith 60 --relevant-triggers --full-saturate-quant
+  trywith 60 --trigger-sel=max --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+  trywith 60 --multi-trigger-cache --full-saturate-quant
+  trywith 60 --no-multi-trigger-linear --full-saturate-quant
+  # other 8min
+  trywith 60 --pre-skolem-quant --full-saturate-quant
+  trywith 60 --inst-when=full --full-saturate-quant
+  trywith 60 --no-e-matching --no-quant-cf --full-saturate-quant
+  trywith 60 --full-saturate-quant --quant-ind
+  trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 60 --decision=internal --full-saturate-quant
+  trywith 60 --term-db-mode=relevant --full-saturate-quant
+  trywith 60 --fs-interleave --full-saturate-quant
+  # finite model find 6min
+  trywith 60 --finite-model-find --mbqi=none
+  trywith 60 --finite-model-find --decision=internal
+  trywith 60 --finite-model-find --macros-quant --macros-quant-mode=all
+  trywith 60 --finite-model-find --uf-ss=no-minimal
+  trywith 120 --finite-model-find --fmf-inst-engine
+  # long runs 8min
+  trywith 480 --finite-model-find --decision=internal
+  finishwith --full-saturate-quant
+  ;;
+ABVFP|BVFP|FP)
+  finishwith --full-saturate-quant --fp-exp
+  ;;
+UFBV)
+  # most problems in UFBV are essentially BV
+  trywith 600 --full-saturate-quant --decision=internal
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
+  finishwith --finite-model-find
+  ;;
+BV)
+  trywith 240 --full-saturate-quant
+  trywith 240 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-bv
+  trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+  # finish 10min
+  finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
+  ;;
+LIA|LRA|NIA|NRA)
+  trywith 60 --full-saturate-quant --nl-ext-tplanes
+  trywith 600 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  trywith 1200
+  finishwith --decision=justification-stoponly
+  ;;
+QF_ABV)
+  trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  trywith 1000 --arrays-weak-equiv
+  finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  ;;
+QF_UFBV)
+  # Benchmarks with uninterpreted sorts cannot be solved with eager
+  # bit-blasting currently
+  trywith 2400 --bitblast=eager --bv-sat-solver=cadical
+  finishwith
+  ;;
+QF_BV)
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  ;;
+QF_AUFLIA)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
+  ;;
+QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
+  ;;
+QF_AUFNIA)
+  finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_ALIA)
+  trywith 140 --decision=justification --arrays-weak-equiv
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_S|QF_SLIA)
+  trywith 300 --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
+  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  ;;
+QF_ABVFP)
+  finishwith --fp-exp
+  ;;
+QF_BVFP)
+  finishwith --fp-exp
+  ;;
+QF_FP)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
new file mode 100755
index 000000000..12c91a036
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -0,0 +1,84 @@
+#!/bin/bash
+
+cvc4=./cvc4
+
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+if [ "$line" != '(set-option :print-success true)' ]; then
+  echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+logic=$(expr "$line" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+if [ -z "$logic" ]; then
+  echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+
+function runcvc4 {
+  # we run in this way for line-buffered input, otherwise memory's a
+  # concern (plus it mimics what we'll end up getting from an
+  # application-track trace runner?)
+  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0-
+}
+
+case "$logic" in
+
+ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA)
+  runcvc4 --incremental
+  ;;
+ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
+  runcvc4 --tear-down-incremental=1
+  ;;
+LIA|LRA)
+  runcvc4 --incremental
+  ;;
+QF_AUFLIA)
+  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
+  ;;
+QF_BV)
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  ;;
+QF_LIA)
+  runcvc4 --tear-down-incremental=1 --unconstrained-simp
+  ;;
+QF_UFBV)
+  runcvc4 --incremental
+  ;;
+QF_UF)
+  runcvc4 --incremental
+  ;;
+QF_AUFBV)
+  runcvc4 --incremental
+  ;;
+QF_ABV)
+  runcvc4 --incremental
+  ;;
+ABVFP)
+  runcvc4 --incremental
+  ;;
+BVFP)
+  runcvc4 --incremental
+  ;;
+QF_ABVFP)
+  runcvc4 --incremental
+  ;;
+QF_BVFP)
+  runcvc4 --incremental
+  ;;
+QF_FP)
+  runcvc4 --incremental
+  ;;
+*)
+  # just run the default
+  runcvc4 --incremental
+  ;;
+
+esac
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
new file mode 100755
index 000000000..eec17294d
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_BV)
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
new file mode 100755
index 000000000..795de734b
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -0,0 +1,86 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_LRA)
+  finishwith --no-restrict-pivots --use-soi --new-prop
+  ;;
+QF_LIA)
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
+  ;;
+QF_NIA)
+  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
+  ;;
+QF_NRA)
+  finishwith --nl-ext --nl-ext-tplanes
+  ;;
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP)
+  finishwith --full-saturate-quant --fp-exp
+  ;;
+UFBV)
+  finishwith --finite-model-find
+  ;;
+BV)
+  finishwith --full-saturate-quant --decision=internal
+  ;;
+LIA|LRA)
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+NIA|NRA)
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  finishwith --decision=justification-stoponly
+  ;;
+QF_ABV)
+  finishwith --ite-simp --simp-with-care --arrays-weak-equiv
+  ;;
+QF_UFBV)
+  finishwith
+  ;;
+QF_BV)
+  finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction
+  ;;
+QF_AUFLIA)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
+  ;;
+QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
+  ;;
+QF_AUFNIA)
+  finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_ALIA)
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_S|QF_SLIA)
+  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  ;;
+QF_ABVFP)
+  finishwith --fp-exp
+  ;;
+QF_BVFP)
+  finishwith --fp-exp
+  ;;
+QF_FP)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/run-script-smtcomp2012 b/contrib/competitions/smt-comp/run-script-smtcomp2012
index dfdd88cc6..dfdd88cc6 100755
--- a/contrib/run-script-smtcomp2012
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2012
diff --git a/contrib/run-script-smtcomp2014 b/contrib/competitions/smt-comp/run-script-smtcomp2014
index 31ee4cf4d..31ee4cf4d 100755
--- a/contrib/run-script-smtcomp2014
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2014
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/competitions/smt-comp/run-script-smtcomp2014-application
index 53df6a927..53df6a927 100755
--- a/contrib/run-script-smtcomp2014-application
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2014-application
diff --git a/contrib/run-script-smtcomp2015 b/contrib/competitions/smt-comp/run-script-smtcomp2015
index 846459f23..846459f23 100755
--- a/contrib/run-script-smtcomp2015
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2015
diff --git a/contrib/run-script-smtcomp2015-application b/contrib/competitions/smt-comp/run-script-smtcomp2015-application
index 3ffcc7234..3ffcc7234 100755
--- a/contrib/run-script-smtcomp2015-application
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2015-application
diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/competitions/smt-comp/run-script-smtcomp2015-assertions
index 4fa96af71..4fa96af71 100755
--- a/contrib/run-script-smtcomp2015-assertions
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2015-assertions
diff --git a/contrib/run-script-smtcomp2016 b/contrib/competitions/smt-comp/run-script-smtcomp2016
index 58b281b4c..58b281b4c 100755
--- a/contrib/run-script-smtcomp2016
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2016
diff --git a/contrib/run-script-smtcomp2016-application b/contrib/competitions/smt-comp/run-script-smtcomp2016-application
index 88bbb5f53..88bbb5f53 100755
--- a/contrib/run-script-smtcomp2016-application
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2016-application
diff --git a/contrib/run-script-smtcomp2017 b/contrib/competitions/smt-comp/run-script-smtcomp2017
index 06cd6a6e4..06cd6a6e4 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2017
diff --git a/contrib/run-script-smtcomp2017-application b/contrib/competitions/smt-comp/run-script-smtcomp2017-application
index 8a8ea7786..8a8ea7786 100755
--- a/contrib/run-script-smtcomp2017-application
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2017-application
diff --git a/contrib/run-script-smtcomp2017-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2017-unsat-cores
index f42f3ca30..f42f3ca30 100644
--- a/contrib/run-script-smtcomp2017-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2017-unsat-cores
diff --git a/contrib/run-script-smtcomp2018 b/contrib/competitions/smt-comp/run-script-smtcomp2018
index 849df0a6b..849df0a6b 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2018
diff --git a/contrib/run-script-smtcomp2018-application b/contrib/competitions/smt-comp/run-script-smtcomp2018-application
index 58db84d36..58db84d36 100755
--- a/contrib/run-script-smtcomp2018-application
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2018-application
diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2018-unsat-cores
index 1454e7a8a..1454e7a8a 100644
--- a/contrib/run-script-smtcomp2018-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2018-unsat-cores
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019 b/contrib/competitions/smt-comp/run-script-smtcomp2019
new file mode 100755
index 000000000..a8c6b0ba4
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2019
@@ -0,0 +1,162 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: trywith [params..]
+# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in which
+# case this run script terminates immediately.  Otherwise, this function
+# returns normally and prints the output of the solver to stderr.
+function trywith {
+  limit=$1; shift;
+  result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+    *)         echo "$result" >&2;;
+  esac
+}
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_LRA)
+  trywith 400 --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi
+  finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp
+  ;;
+QF_LIA)
+  # same as QF_LRA but add --pb-rewrites
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
+  ;;
+QF_NIA)
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 60 --nl-ext-tplanes --decision=justification
+  trywith 60 --no-nl-ext-tplanes --decision=internal
+  # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail
+  trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  finishwith --nl-ext-tplanes --decision=internal
+  ;;
+QF_NRA)
+  trywith 600 --nl-ext-tplanes --decision=internal
+  trywith 600 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 60 --nl-ext-tplanes --decision=internal --solve-real-as-int
+  finishwith --nl-ext-tplanes --decision=justification
+  ;;
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA)
+  # the following is designed for a run time of 20 min.
+  # initial runs 2min
+  trywith 60 --simplification=none --full-saturate-quant
+  trywith 60 --no-e-matching --full-saturate-quant
+  # trigger selections 6min
+  trywith 60 --relevant-triggers --full-saturate-quant
+  trywith 60 --trigger-sel=max --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --full-saturate-quant
+  trywith 60 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+  trywith 60 --multi-trigger-cache --full-saturate-quant
+  trywith 60 --no-multi-trigger-linear --full-saturate-quant
+  # other 8min
+  trywith 60 --pre-skolem-quant --full-saturate-quant
+  trywith 60 --inst-when=full --full-saturate-quant
+  trywith 60 --no-e-matching --no-quant-cf --full-saturate-quant
+  trywith 60 --full-saturate-quant --quant-ind
+  trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 60 --decision=internal --full-saturate-quant
+  trywith 60 --term-db-mode=relevant --full-saturate-quant
+  trywith 60 --fs-interleave --full-saturate-quant
+  # finite model find 6min
+  trywith 60 --finite-model-find --mbqi=none
+  trywith 60 --finite-model-find --decision=internal
+  trywith 60 --finite-model-find --macros-quant --macros-quant-mode=all
+  trywith 60 --finite-model-find --uf-ss=no-minimal
+  trywith 120 --finite-model-find --fmf-inst-engine
+  # long runs 8min
+  trywith 480 --finite-model-find --decision=internal
+  finishwith --full-saturate-quant
+  ;;
+ABVFP|BVFP|FP)
+  finishwith --full-saturate-quant --fp-exp
+  ;;
+UFBV)
+  # most problems in UFBV are essentially BV
+  trywith 600 --full-saturate-quant --decision=internal
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
+  finishwith --finite-model-find
+  ;;
+BV)
+  trywith 240 --full-saturate-quant
+  trywith 240 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cbqi-bv
+  trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+  # finish 10min
+  finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
+  ;;
+LIA|LRA|NIA|NRA)
+  trywith 60 --full-saturate-quant --nl-ext-tplanes
+  trywith 600 --full-saturate-quant --no-cbqi-innermost
+  trywith 600 --full-saturate-quant --cbqi-nested-qe
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  trywith 1200
+  finishwith --decision=justification-stoponly
+  ;;
+QF_ABV)
+  trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  trywith 1000 --arrays-weak-equiv
+  finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  ;;
+QF_UFBV)
+  # Benchmarks with uninterpreted sorts cannot be solved with eager
+  # bit-blasting currently
+  trywith 2400 --bitblast=eager --bv-sat-solver=cadical
+  finishwith
+  ;;
+QF_BV)
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  ;;
+QF_AUFLIA)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
+  ;;
+QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
+  ;;
+QF_AUFNIA)
+  finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_ALIA)
+  trywith 140 --decision=justification --arrays-weak-equiv
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_S|QF_SLIA)
+  trywith 300 --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
+  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  ;;
+QF_ABVFP)
+  finishwith --fp-exp
+  ;;
+QF_BVFP)
+  finishwith --fp-exp
+  ;;
+QF_FP)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019-incremental b/contrib/competitions/smt-comp/run-script-smtcomp2019-incremental
new file mode 100755
index 000000000..12c91a036
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2019-incremental
@@ -0,0 +1,84 @@
+#!/bin/bash
+
+cvc4=./cvc4
+
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+if [ "$line" != '(set-option :print-success true)' ]; then
+  echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+logic=$(expr "$line" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+if [ -z "$logic" ]; then
+  echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+
+function runcvc4 {
+  # we run in this way for line-buffered input, otherwise memory's a
+  # concern (plus it mimics what we'll end up getting from an
+  # application-track trace runner?)
+  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0-
+}
+
+case "$logic" in
+
+ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA)
+  runcvc4 --incremental
+  ;;
+ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
+  runcvc4 --tear-down-incremental=1
+  ;;
+LIA|LRA)
+  runcvc4 --incremental
+  ;;
+QF_AUFLIA)
+  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
+  ;;
+QF_BV)
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  ;;
+QF_LIA)
+  runcvc4 --tear-down-incremental=1 --unconstrained-simp
+  ;;
+QF_UFBV)
+  runcvc4 --incremental
+  ;;
+QF_UF)
+  runcvc4 --incremental
+  ;;
+QF_AUFBV)
+  runcvc4 --incremental
+  ;;
+QF_ABV)
+  runcvc4 --incremental
+  ;;
+ABVFP)
+  runcvc4 --incremental
+  ;;
+BVFP)
+  runcvc4 --incremental
+  ;;
+QF_ABVFP)
+  runcvc4 --incremental
+  ;;
+QF_BVFP)
+  runcvc4 --incremental
+  ;;
+QF_FP)
+  runcvc4 --incremental
+  ;;
+*)
+  # just run the default
+  runcvc4 --incremental
+  ;;
+
+esac
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp2019-model-validation
new file mode 100755
index 000000000..eec17294d
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2019-model-validation
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_BV)
+  finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores
new file mode 100755
index 000000000..795de734b
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2019-unsat-cores
@@ -0,0 +1,86 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_LRA)
+  finishwith --no-restrict-pivots --use-soi --new-prop
+  ;;
+QF_LIA)
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
+  ;;
+QF_NIA)
+  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
+  ;;
+QF_NRA)
+  finishwith --nl-ext --nl-ext-tplanes
+  ;;
+# all logics with UF + quantifiers should either fall under this or special cases below
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP)
+  finishwith --full-saturate-quant --fp-exp
+  ;;
+UFBV)
+  finishwith --finite-model-find
+  ;;
+BV)
+  finishwith --full-saturate-quant --decision=internal
+  ;;
+LIA|LRA)
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+NIA|NRA)
+  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  finishwith --decision=justification-stoponly
+  ;;
+QF_ABV)
+  finishwith --ite-simp --simp-with-care --arrays-weak-equiv
+  ;;
+QF_UFBV)
+  finishwith
+  ;;
+QF_BV)
+  finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction
+  ;;
+QF_AUFLIA)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
+  ;;
+QF_AX)
+  finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
+  ;;
+QF_AUFNIA)
+  finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_ALIA)
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_S|QF_SLIA)
+  finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
+  ;;
+QF_ABVFP)
+  finishwith --fp-exp
+  ;;
+QF_BVFP)
+  finishwith --fp-exp
+  ;;
+QF_FP)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/run-script-smteval2013 b/contrib/competitions/smt-comp/run-script-smteval2013
index 2212f71c7..2212f71c7 100755
--- a/contrib/run-script-smteval2013
+++ b/contrib/competitions/smt-comp/run-script-smteval2013
diff --git a/contrib/run-script-sygusComp2016-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2016-CLIA
index 3dc08d8c0..3dc08d8c0 100755
--- a/contrib/run-script-sygusComp2016-CLIA
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-CLIA
diff --git a/contrib/run-script-sygusComp2016-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2016-GENERAL
index 0ee133ea8..0ee133ea8 100755
--- a/contrib/run-script-sygusComp2016-GENERAL
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-GENERAL
diff --git a/contrib/run-script-sygusComp2016-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2016-INV
index a25a5f5c8..a25a5f5c8 100755
--- a/contrib/run-script-sygusComp2016-INV
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-INV
diff --git a/contrib/run-script-sygusComp2016-PBE b/contrib/competitions/sygus-comp/run-script-sygusComp2016-PBE
index 19d8fd891..19d8fd891 100755
--- a/contrib/run-script-sygusComp2016-PBE
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2016-PBE
diff --git a/contrib/run-script-sygusComp2017-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2017-CLIA
index 3dc08d8c0..3dc08d8c0 100755
--- a/contrib/run-script-sygusComp2017-CLIA
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-CLIA
diff --git a/contrib/run-script-sygusComp2017-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2017-GENERAL
index 0ee133ea8..0ee133ea8 100755
--- a/contrib/run-script-sygusComp2017-GENERAL
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-GENERAL
diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2017-INV
index a21792fb9..a21792fb9 100755
--- a/contrib/run-script-sygusComp2017-INV
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-INV
diff --git a/contrib/run-script-sygusComp2017-PBE_BitVec b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_BitVec
index 19d8fd891..19d8fd891 100755
--- a/contrib/run-script-sygusComp2017-PBE_BitVec
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_BitVec
diff --git a/contrib/run-script-sygusComp2017-PBE_Strings b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_Strings
index 849835b28..849835b28 100755
--- a/contrib/run-script-sygusComp2017-PBE_Strings
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2017-PBE_Strings
diff --git a/contrib/run-script-sygusComp2018-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2018-CLIA
index b4e00423c..b4e00423c 100644
--- a/contrib/run-script-sygusComp2018-CLIA
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-CLIA
diff --git a/contrib/run-script-sygusComp2018-GENERAL b/contrib/competitions/sygus-comp/run-script-sygusComp2018-GENERAL
index 8419e6841..8419e6841 100644
--- a/contrib/run-script-sygusComp2018-GENERAL
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-GENERAL
diff --git a/contrib/run-script-sygusComp2018-INV b/contrib/competitions/sygus-comp/run-script-sygusComp2018-INV
index 57870a5af..57870a5af 100644
--- a/contrib/run-script-sygusComp2018-INV
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-INV
diff --git a/contrib/run-script-sygusComp2018-PBE_BitVec b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_BitVec
index ee5035e59..ee5035e59 100644
--- a/contrib/run-script-sygusComp2018-PBE_BitVec
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_BitVec
diff --git a/contrib/run-script-sygusComp2018-PBE_Strings b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_Strings
index a9e05bf76..a9e05bf76 100644
--- a/contrib/run-script-sygusComp2018-PBE_Strings
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2018-PBE_Strings
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA
new file mode 100755
index 000000000..97bb2175b
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-CLIA
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --cegqi-si=all --cegqi-si-abort --cbqi --cbqi-prereg-inst
+trywith 10 --cegqi-si=none --sygus-repair-const
+finishwith --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto
new file mode 100755
index 000000000..36afb0790
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-auto
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --cegqi-si=all --cegqi-si-abort --cbqi --cbqi-prereg-inst
+trywith 5 --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f
new file mode 100755
index 000000000..5c5e5e9e7
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-f
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 5 --sygus-active-gen=enum --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=enum --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s
new file mode 100755
index 000000000..2a19a14b5
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-GENERAL-s
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 5 --sygus-active-gen=none --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=none --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f
new file mode 100755
index 000000000..21120c0a4
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-f
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 10 --sygus-active-gen=enum --sygus-repair-const
+trywith 120 --sygus-unif
+finishwith --sygus-active-gen=enum
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s
new file mode 100755
index 000000000..e835ba91a
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-s
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 10 --sygus-active-gen=none --sygus-repair-const
+trywith 120 --sygus-unif
+finishwith --sygus-active-gen=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su
new file mode 100755
index 000000000..b3e056d7c
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-INV-su
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 30 --sygus-unif-boolean-heuristic-dt --sygus-active-gen=var-agnostic --sygus-add-const-grammar --decision=justification
+trywith 10 --sygus-active-gen=none --sygus-repair-const
+finishwith --sygus-active-gen=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f
new file mode 100755
index 000000000..7fd203238
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s
new file mode 100755
index 000000000..27d72f7a0
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_BitVec-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --sygus-active-gen=none --cegqi-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f
new file mode 100755
index 000000000..f60263e05
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --cegqi-si=none --sygus-fair=direct
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s
new file mode 100755
index 000000000..42c7c40e7
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp2019-PBE_Strings-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --sygus-active-gen=none --cegqi-si=none --sygus-fair=direct
diff --git a/contrib/run-script-syguscomp2015 b/contrib/competitions/sygus-comp/run-script-syguscomp2015
index aab6851e1..aab6851e1 100755
--- a/contrib/run-script-syguscomp2015
+++ b/contrib/competitions/sygus-comp/run-script-syguscomp2015
diff --git a/contrib/get-abc b/contrib/get-abc
index fa90f240f..5d3f32fb5 100755
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 670fc3b41..ecc92d998 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 ANTLR_HOME_DIR=antlr-3.4
@@ -34,7 +34,7 @@ cd $ANTLR_HOME_DIR || exit 1
 webget https://www.antlr3.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar 
 webget https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz
 tee bin/antlr3 <<EOF
-#!/bin/bash
+#!/usr/bin/env bash
 export CLASSPATH=`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
 exec java org.antlr.Tool "\$@"
 EOF
@@ -46,7 +46,7 @@ cd libantlr3c-3.4
 
 # Use an absolute path for the installation directory to avoid spurious libtool
 # warnings about the ANTLR library having moved
-PREFIX=$(realpath `pwd`/../..)
+PREFIX=$($PYTHON -c "import os; print(os.path.realpath('$(pwd)/../..'))")
 
 # Make antlr3debughandlers.c empty to avoid unreferenced symbols
 rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c
diff --git a/contrib/get-authors b/contrib/get-authors
index d70e0ecda..df147d10d 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -66,6 +66,7 @@ while [ $# -gt 0 ]; do
     sed 's/Martin/Martin Brain/' | \
     sed 's/justinxu421/Justin Xu/' | \
     sed 's/yoni206/Yoni Zohar/' | \
+    sed 's/ayveejay/Andrew V. Jones/' | \
 
     # Remove first columns from uniq -c (number of lines)
     awk '{$1=""; print}' | \
diff --git a/contrib/get-cadical b/contrib/get-cadical
index 359afaaa7..6cc1208c6 100755
--- a/contrib/get-cadical
+++ b/contrib/get-cadical
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
@@ -7,11 +7,13 @@ if [ -e cadical ]; then
   exit 1
 fi
 
-commit="b44ce4f0e64aa400358ae3a8adb45b24ae6e742c"
+version="rel-1.0.3"
 
-git clone https://github.com/arminbiere/cadical cadical
+webget "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "cadical-$version.tar.gz"
+tar xfvz "cadical-$version.tar.gz"
+rm "cadical-$version.tar.gz"
+mv "cadical-$version" cadical
 cd cadical
-git checkout $commit
 
 CXXFLAGS="-fPIC" ./configure && make -j$(nproc)
 
diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat
index 6b3a7029a..379d75df1 100755
--- a/contrib/get-cryptominisat
+++ b/contrib/get-cryptominisat
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
diff --git a/contrib/get-drat2er b/contrib/get-drat2er
index e465ab3d4..52c663ab3 100755
--- a/contrib/get-drat2er
+++ b/contrib/get-drat2er
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 if [ -e drat2er ]; then
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index dcd5aac00..85ea643a9 100755
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
diff --git a/contrib/get-gmp b/contrib/get-gmp
index 02602e456..aec125185 100755
--- a/contrib/get-gmp
+++ b/contrib/get-gmp
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # This script should only be used if your distribution does not ship with the
 # GMP configuration you need. For example, contrib/get-win-dependencies
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 2fc191707..953d05d18 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
@@ -6,7 +6,7 @@ lfscrepo="https://github.com/CVC4/LFSC.git"
 dirname="lfsc-checker"
 
 function gitclone {
-  if which git &> /dev/null
+  if [ -x "$(command -v git)" ]
   then
     git clone "$1" "$2"
   else
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh
index de4a93587..4e2a133b3 100644
--- a/contrib/get-script-header.sh
+++ b/contrib/get-script-header.sh
@@ -1,6 +1,6 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
-set -e
+set -e -o pipefail
 
 cd "$(dirname "$0")/.."
 
@@ -15,12 +15,24 @@ if ! [ -e src/parser/cvc/Cvc.g ]; then
 fi
 
 function webget {
-  if which wget &>/dev/null; then
+  if [ -x "$(command -v wget)" ]; then
     wget -c -O "$2" "$1"
-  elif which curl &>/dev/null; then
+  elif [ -x "$(command -v curl)" ]; then
     curl -L "$1" >"$2"
   else
     echo "Can't figure out how to download from web.  Please install wget or curl." >&2
     exit 1
   fi
 }
+
+for cmd in python python2 python3; do
+  if [ -x "$(command -v $cmd)" ]; then
+    PYTHON="$cmd"
+    break
+  fi
+done
+
+if [ -z "$PYTHON" ]; then
+  echo "Error: Couldn't find python, python2, or python3." >&2
+  exit 1
+fi
diff --git a/contrib/get-symfpu b/contrib/get-symfpu
index 705e9d873..b17c00299 100755
--- a/contrib/get-symfpu
+++ b/contrib/get-symfpu
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
@@ -9,7 +9,7 @@ if [ -e $wdir ]; then
   exit 1
 fi
 
-commit="1273dc9379b36af1461fe04aa453db82408006cf"
+commit="8fbe139bf0071cbe0758d2f6690a546c69ff0053"
 
 mkdir $wdir
 cd $wdir
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index f3fbd6cf7..1138e3071 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -1,10 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 # win32-build script
 # Morgan Deters <mdeters@cs.nyu.edu>
 # Tue, 15 Jan 2013 11:11:24 -0500
 #
 
+set -e -o pipefail
+
 export WINDOWS_BUILD=yes
 export MAKE_CFLAGS=
 export MAKE_CXXFLAGS=
@@ -50,10 +52,10 @@ function reporterror {
 }
 
 function webget {
-  if which curl &>/dev/null; then
-    curl -L "$1" >"$2"
-  elif which wget &>/dev/null; then
+  if [ -x "$(command -v wget)" ]; then
     wget -c -O "$2" "$1"
+  elif [ -x "$(command -v curl)" ]; then
+    curl -L "$1" >"$2"
   else
     echo "Can't figure out how to download from web.  Please install wget or curl." >&2
     exit 1