Update competition scripts (#4715)

This PR creates a "current" sygus comp scripts, similar to what we have been doing for SMT COMP. It updates these scripts to fix the option names, as many have changed recently.

This also copies the SMT COMP current scripts to 2020, since they were used in the current state. @4tXJ7f let me know if this is not the case.

15 files changed, 691 insertions, 0 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2020 b/contrib/competitions/smt-comp/run-script-smtcomp2020
new file mode 100644
index 000000000..3ca8bd32b
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2020
@@ -0,0 +1,183 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+# Output other than "sat"/"unsat" is either written to stderr or to "err.log"
+# in the directory specified by $2 if it has been set (e.g. when running on
+# StarExec).
+out_file=/dev/stderr
+
+if [ -n "$STAREXEC_WALLCLOCK_LIMIT" ]; then
+  # If we are running on StarExec, don't print to `/dev/stderr/` even when $2
+  # is not provided.
+  out_file="/dev/null"
+fi
+
+if [ -n "$2" ]; then
+  out_file="$2/err.log"
+fi
+
+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 $out_file.
+function trywith {
+  limit=$1; shift;
+  result="$({ ulimit -S -t "$limit"; $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+    *)         echo "$result" &> "$out_file";;
+  esac
+}
+
+# use: finishwith [params..]
+# to run cvc4. Only "sat" or "unsat" are output. Other outputs are written to
+# $out_file.
+function finishwith {
+  result="$({ $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+    *)         echo "$result" &> "$out_file";;
+  esac
+}
+
+# the following is designed for a run time of 20 min.
+case "$logic" in
+
+QF_LRA)
+  trywith 200 --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 --ite-simp --simp-ite-compress
+  ;;
+QF_NIA)
+  trywith 480 --nl-ext-tplanes --decision=internal
+  trywith 60 --nl-ext-tplanes --decision=justification
+  trywith 60 --no-nl-ext-tplanes --decision=internal
+  trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal
+  # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
+  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
+  finishwith --nl-ext-tplanes --decision=internal
+  ;;
+QF_NRA)
+  trywith 300 --nl-ext-tplanes --decision=internal
+  trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 30 --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)
+  # initial runs 1 min
+  trywith 30 --simplification=none --full-saturate-quant
+  trywith 30 --no-e-matching --full-saturate-quant
+  # trigger selections 3 min
+  trywith 30 --relevant-triggers --full-saturate-quant
+  trywith 30 --trigger-sel=max --full-saturate-quant
+  trywith 30 --multi-trigger-when-single --full-saturate-quant
+  trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant
+  trywith 30 --multi-trigger-cache --full-saturate-quant
+  trywith 30 --no-multi-trigger-linear --full-saturate-quant
+  # other 4 min
+  trywith 30 --pre-skolem-quant --full-saturate-quant
+  trywith 30 --inst-when=full --full-saturate-quant
+  trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
+  trywith 30 --full-saturate-quant --quant-ind
+  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 30 --decision=internal --full-saturate-quant
+  trywith 30 --term-db-mode=relevant --full-saturate-quant
+  trywith 30 --fs-interleave --full-saturate-quant
+  # finite model find 3 min
+  trywith 30 --finite-model-find --mbqi=none
+  trywith 30 --finite-model-find --decision=internal
+  trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all
+  trywith 30 --finite-model-find --uf-ss=no-minimal
+  trywith 60 --finite-model-find --fmf-inst-engine
+  # long runs 4 min
+  trywith 240 --finite-model-find --decision=internal
+  finishwith --full-saturate-quant
+  ;;
+ABVFP|BVFP|FP|UFFPDTLIRA|UFFPDTNIRA)
+  finishwith --full-saturate-quant --fp-exp
+  ;;
+UFBV)
+  # most problems in UFBV are essentially BV
+  trywith 300 --full-saturate-quant --decision=internal
+  trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate
+  finishwith --finite-model-find
+  ;;
+BV)
+  trywith 120 --full-saturate-quant
+  trywith 120 --full-saturate-quant --no-cegqi-innermost
+  trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 30 --full-saturate-quant --no-cegqi-bv
+  trywith 30 --full-saturate-quant --cegqi-bv-ineq=eq-slack
+  # finish 10min
+  finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
+  ;;
+LIA|LRA|NIA|NRA)
+  trywith 30 --full-saturate-quant --nl-ext-tplanes
+  trywith 300 --full-saturate-quant --no-cegqi-innermost
+  trywith 300 --full-saturate-quant --cegqi-nested-qe
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  trywith 600 --ite-simp
+  finishwith --decision=justification-stoponly --ite-simp
+  ;;
+QF_ABV)
+  trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
+  trywith 500 --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 1200 --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 --strings-fmf
+  finishwith --strings-exp --rewrite-divk
+  ;;
+QF_ABVFP|QF_ABVFPLRA)
+  finishwith --fp-exp
+  ;;
+QF_BVFP|QF_BVFPLRA)
+  finishwith --fp-exp
+  ;;
+QF_FP|QF_FPLRA)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental
new file mode 100644
index 000000000..7861a4c85
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental
@@ -0,0 +1,75 @@
+#!/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-type-checking --no-interactive "$@" <&0-
+}
+
+case "$logic" in
+
+ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA)
+  runcvc4 --tear-down-incremental=1
+  ;;
+QF_AUFLIA)
+  runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_BV)
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  ;;
+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-smtcomp2020-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp2020-model-validation
new file mode 100644
index 000000000..9982a9e29
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2020-model-validation
@@ -0,0 +1,30 @@
+#!/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-type-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 --pb-rewrites --ite-simp --simp-ite-compress
+  ;;
+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-smtcomp2020-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp2020-unsat-cores
new file mode 100644
index 000000000..b5449470f
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2020-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-type-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 --ite-simp --simp-ite-compress
+  ;;
+QF_NIA)
+  finishwith --nl-ext --nl-ext-tplanes
+  ;;
+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 --cegqi-nested-qe --decision=internal
+  ;;
+NIA|NRA)
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
+  ;;
+QF_AUFBV)
+  finishwith --decision=justification-stoponly --ite-simp
+  ;;
+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
+  ;;
+QF_ABVFP|QF_ABVFPLRA)
+  finishwith --fp-exp
+  ;;
+QF_BVFP|QF_BVFPLRA)
+  finishwith --fp-exp
+  ;;
+QF_FP|QF_FPLRA)
+  finishwith --fp-exp
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA
new file mode 100755
index 000000000..d9864f651
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-type-checking --no-interactive --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-type-checking --no-interactive --dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --sygus-si=all --sygus-si-abort --ceqqi-prereg-inst
+trywith 10 --sygus-si=none --sygus-repair-const
+finishwith --sygus-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto b/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto
new file mode 100755
index 000000000..f69398bed
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --sygus-si=all --sygus-si-abort --cegqi-prereg-inst
+trywith 5 --sygus-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-f b/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-f
new file mode 100755
index 000000000..b7594b348
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --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 --sygus-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=enum --sygus-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-s b/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-s
new file mode 100755
index 000000000..fdb1f440d
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --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 --sygus-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=none --sygus-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-f b/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-f
new file mode 100755
index 000000000..03e676e78
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --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-pi=complete
+finishwith --sygus-active-gen=enum
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-s b/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-s
new file mode 100755
index 000000000..79e8c19bf
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --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-pi=complete
+finishwith --sygus-active-gen=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-su b/contrib/competitions/sygus-comp/run-script-sygusComp-current-INV-su
new file mode 100755
index 000000000..61efcf6c0
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-type-checking --no-interactive --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-type-checking --no-interactive --dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 30 --sygus-unif-pi=cond-enum-igain --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-sygusComp-current-PBE_BitVec-f b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_BitVec-f
new file mode 100755
index 000000000..e5c55bc2e
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_BitVec-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-type-checking --no-interactive --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-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_BitVec-s b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_BitVec-s
new file mode 100755
index 000000000..b70f9a478
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_BitVec-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-type-checking --no-interactive --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 --sygus-si=none
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-f b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-f
new file mode 100755
index 000000000..21c66a7b0
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-type-checking --no-interactive --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-si=none --sygus-fair=direct
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-s b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-s
new file mode 100755
index 000000000..fa5018a04
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-PBE_Strings-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-type-checking --no-interactive --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 --sygus-si=none --sygus-fair=direct