Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

14 files changed, 516 insertions, 0 deletions

diff --git a/contrib/cryptominisat-4.2.0.patch b/contrib/cryptominisat-4.2.0.patch
new file mode 100644
index 000000000..30b24a3cc
--- /dev/null
+++ b/contrib/cryptominisat-4.2.0.patch
@@ -0,0 +1,12 @@
+diff -ruN orig/CMakeLists.txt new/CMakeLists.txt
+--- CMakeLists.txt	2016-05-24 22:05:50.702570824 -0700
++++ patched.txt	2016-05-24 22:05:57.778570529 -0700
+@@ -132,7 +132,7 @@
+     set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
+     SET(Boost_USE_STATIC_LIBS ON)
+     set(CMAKE_EXE_LINKER_FLAGS "-static -Wl,--whole-archive -lpthread -Wl,--no-whole-archive")
+-
++    add_cxx_flag_if_supported("-fPIC")
+     set(NOMYSQL ON)
+ else()
+     add_definitions(-DBOOST_TEST_DYN_LINK)
diff --git a/contrib/cryptominisat-4.2.0.second.patch b/contrib/cryptominisat-4.2.0.second.patch
new file mode 100644
index 000000000..4b3fdf722
--- /dev/null
+++ b/contrib/cryptominisat-4.2.0.second.patch
@@ -0,0 +1,11 @@
+--- python/CMakeLists.txt	2016-05-24 22:05:50.698570824 -0700
++++ ../new/python/CMakeLists.txt	2016-05-24 22:05:57.774570529 -0700
+@@ -12,7 +12,7 @@
+ 
+ add_custom_target(pytarget ALL DEPENDS ${OUTPUT}/timestamp)
+ 
+-install(CODE "execute_process(COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --record files.txt)")
++#install(CODE "execute_process(COMMAND ${PYTHON_EXECUTABLE} ${SETUP_PY} install --record files.txt)")
+ 
+ if (ENABLE_TESTING)
+     #add_test (pytest ${PYTHON_EXECUTABLE} "${CMAKE_CURRENT_SOURCE_DIR}/test_pycryptosat.py")
diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
new file mode 100755
index 000000000..c96bbe03d
--- /dev/null
+++ b/contrib/get-cryptominisat4
@@ -0,0 +1,57 @@
+#!/bin/bash
+#
+set -e
+
+version="4.2.0"
+
+cd "$(dirname "$0")/.."
+
+if ! [ -e src/parser/cvc/Cvc.g ]; then
+  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
+  echo "but apparently:" >&2
+  echo >&2
+  echo "  $(pwd)" >&2
+  echo >&2
+  echo "is not a CVC4 source tree ?!" >&2
+  exit 1
+fi
+
+function webget {
+  if which wget &>/dev/null; then
+    wget -c -O "$2" "$1"
+  elif which curl &>/dev/null; then
+    curl "$1" >"$2"
+  else
+    echo "Can't figure out how to download from web.  Please install wget or curl." >&2
+    exit 1
+  fi
+}
+
+if [ -e cryptominisat4 ]; then
+  echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+mkdir cryptominisat4
+cd cryptominisat4
+CRYPTOMINISAT_PATH=`pwd`
+
+webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz
+gunzip -f cryptominisat-$version.tar.gz
+tar xfv cryptominisat-$version.tar
+cd cryptominisat-$version
+
+patch -p0 < ../../contrib/cryptominisat-4.2.0.patch
+patch -p0 < ../../contrib/cryptominisat-4.2.0.second.patch 
+
+mkdir ../build
+cd ../build
+
+cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" -DNOM4RI="ON"  ../cryptominisat-$version
+make install -j2
+
+cd ../
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-cryptominisat --with-cryptominisat-dir=`pwd`
diff --git a/contrib/lfsc_lsan.supp b/contrib/lfsc_lsan.supp
new file mode 100644
index 000000000..63022a8f9
--- /dev/null
+++ b/contrib/lfsc_lsan.supp
@@ -0,0 +1,8 @@
+# LSAN suppressions for memory leaks in LFSC.
+#
+# To use this file, add LSAN_OPTIONS to the commandline invocation.
+#   LSAN_OPTIONS=suppressions=contrib/lfsc_lsan.supp ./build/bin/cvc4 ...
+# For more information on the leak sanitizer in ASAN, see
+# https://github.com/google/sanitizers/wiki/AddressSanitizerLeakSanitizer
+leak:CVC4::CnfProof::pushCurrentDefinition
+
diff --git a/contrib/run-script-cascj8-fnt b/contrib/run-script-cascj8-fnt
new file mode 100644
index 000000000..bc37180a6
--- /dev/null
+++ b/contrib/run-script-cascj8-fnt
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j8 : $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 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 60 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --sort-inference --uf-ss-fair
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj8-fof b/contrib/run-script-cascj8-fof
new file mode 100644
index 000000000..fe18c3ed0
--- /dev/null
+++ b/contrib/run-script-cascj8-fof
@@ -0,0 +1,48 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fof casc j8 : $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 --relational-triggers --full-saturate-quant 
+trywith 20 --no-e-matching --full-saturate-quant 
+trywith 15 --finite-model-find --mbqi=abs
+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 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
+trywith 10 --term-db-mode=relevant --full-saturate-quant
+trywith 15 --prenex-quant=none --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --relevant-triggers --full-saturate-quant 
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair
+trywith 30 --fs-inst --full-saturate-quant
+trywith 30 --no-quant-cf --full-saturate-quant 
+finishwith --qcf-vo-exp --full-saturate-quant 
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj8-tfa b/contrib/run-script-cascj8-tfa
new file mode 100644
index 000000000..da4056466
--- /dev/null
+++ b/contrib/run-script-cascj8-tfa
@@ -0,0 +1,40 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfa casc j8 : $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 10 --decision=internal --full-saturate-quant
+trywith 10 --finite-model-find --decision=internal
+trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --partial-triggers --full-saturate-quant
+trywith 10 --no-e-matching --full-saturate-quant
+trywith 30 --cbqi-all --purify-triggers --full-saturate-quant 
+trywith 60 --cbqi-all --fs-inst --full-saturate-quant
+finishwith --full-saturate-quant
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj8-tfn b/contrib/run-script-cascj8-tfn
new file mode 100644
index 000000000..a6fe1e23c
--- /dev/null
+++ b/contrib/run-script-cascj8-tfn
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-fnt casc j8 : $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 60 --finite-model-find --sort-inference --uf-ss-fair
+trywith 30 --full-saturate-quant
+trywith 30 --finite-model-find --fmf-bound-int --macros-quant
+finishwith --finite-model-find --decision=internal --sort-inference --uf-ss-fair
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016
new file mode 100644
index 000000000..58b281b4c
--- /dev/null
+++ b/contrib/run-script-smtcomp2016
@@ -0,0 +1,134 @@
+#!/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.
+function trywith {
+  limit=$1; shift;
+  result="$(ulimit -S -t "$limit";$cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+  esac
+}
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_LRA)
+  trywith 200 --enable-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 --enable-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 20
+  trywith 1800 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat
+  trywith 1800 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat
+  trywith 1800 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat
+  trywith 1800 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat
+  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
+  ;;
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA)
+  # the following is designed for a run time of 2400s (40 min).
+  # initial runs 1min
+  trywith 20 --simplification=none --full-saturate-quant
+  trywith 20 --no-e-matching --full-saturate-quant
+  trywith 20 --fs-inst --decision=internal --full-saturate-quant
+  # trigger selections 2min
+  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
+  # other 2min
+  trywith 30 --pre-skolem-quant --full-saturate-quant
+  trywith 30 --inst-when=full --full-saturate-quant
+  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
+  trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
+  # finite model find 2min
+  trywith 30 --finite-model-find
+  trywith 30 --finite-model-find --uf-ss=no-minimal
+  trywith 60 --finite-model-find --decision=internal
+  # long runs 20min
+  trywith 300 --decision=internal --full-saturate-quant
+  trywith 300 --term-db-mode=relevant --full-saturate-quant
+  trywith 300 --fs-inst --full-saturate-quant
+  trywith 300 --finite-model-find --fmf-inst-engine
+  # finite model find 1min
+  trywith 30 --finite-model-find --fmf-bound-int
+  trywith 30 --finite-model-find --sort-inference
+  # finish 12min
+  finishwith --full-saturate-quant
+  ;;
+UFBV)
+  # many problems in UFBV are essentially BV
+  trywith 300 --full-saturate-quant 
+  trywith 300 --finite-model-find
+  finishwith --cbqi-all --full-saturate-quant
+  ;;
+BV)
+  trywith 300 --finite-model-find
+  finishwith --cbqi-all --full-saturate-quant
+  ;;
+LIA|LRA|NIA|NRA)
+  trywith 30 --full-saturate-quant
+  trywith 300 --full-saturate-quant --cbqi-min-bounds
+  trywith 300 --full-saturate-quant --decision=internal
+  finishwith --full-saturate-quant --cbqi-midpoint
+  ;;
+QF_AUFBV)
+  trywith 600
+  finishwith --decision=justification-stoponly
+  ;;
+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)
+  finishwith --bitblast=eager --bv-sat-solver=cryptominisat
+  ;;
+QF_BV)
+  exec ./pcvc4 -L smt2 --no-incremental --no-checking --no-interactive --thread-stack=1024 \
+         --threads 2 \
+         --thread0 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager  --bv-sat-solver=cryptominisat --bitblast-aig --no-bv-abstraction' \
+         --thread1 '--unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bv-eq-slicer=auto --no-bv-abstraction' \
+         --no-wait-to-join \
+         "$bench"
+  #trywith 10 --bv-eq-slicer=auto --decision=justification
+  #trywith 60 --decision=justification
+  #trywith 600 --decision=internal --bitblast-eager
+  #finishwith --decision=justification --decision-use-weight --decision-weight-internal=usr1
+  ;;
+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 70 --decision=justification --arrays-weak-equiv
+  finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+
diff --git a/contrib/run-script-smtcomp2016-application b/contrib/run-script-smtcomp2016-application
new file mode 100644
index 000000000..88bbb5f53
--- /dev/null
+++ b/contrib/run-script-smtcomp2016-application
@@ -0,0 +1,51 @@
+#!/bin/bash
+
+cvc4=./cvc4-application
+
+read line
+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
+read line
+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 --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)
+  runcvc4 --tear-down-incremental=1
+  ;;
+LIA)
+  runcvc4 --incremental --cbqi
+  ;;
+QF_AUFLIA)
+  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
+  ;;
+QF_BV)
+  runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
+  ;;
+QF_LIA)
+  runcvc4 --tear-down-incremental=1 --unconstrained-simp
+  ;;
+*)
+  # just run the default
+  runcvc4 --incremental
+  ;;
+
+esac
diff --git a/contrib/run-script-sygusComp2016-CLIA b/contrib/run-script-sygusComp2016-CLIA
new file mode 100644
index 000000000..3dc08d8c0
--- /dev/null
+++ b/contrib/run-script-sygusComp2016-CLIA
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function trywith {
+  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --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
+}
+
+trywith --decision=internal --cbqi-prereg-inst
+ 
diff --git a/contrib/run-script-sygusComp2016-GENERAL b/contrib/run-script-sygusComp2016-GENERAL
new file mode 100755
index 000000000..0ee133ea8
--- /dev/null
+++ b/contrib/run-script-sygusComp2016-GENERAL
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |
+    (read result w1;
+    case "$result" in
+    unsat) echo "$w1";cat;exit 0;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi  
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --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-abort --cegqi-si-abort --decision=internal --cbqi-prereg-inst
+finishwith --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2016-INV b/contrib/run-script-sygusComp2016-INV
new file mode 100644
index 000000000..a25a5f5c8
--- /dev/null
+++ b/contrib/run-script-sygusComp2016-INV
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function trywith {
+  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --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
+}
+
+trywith --sygus-inv-templ=post
+ 
diff --git a/contrib/run-script-sygusComp2016-PBE b/contrib/run-script-sygusComp2016-PBE
new file mode 100644
index 000000000..19d8fd891
--- /dev/null
+++ b/contrib/run-script-sygusComp2016-PBE
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function trywith {
+  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --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
+}
+
+trywith --cegqi-si=none
+