summaryrefslogtreecommitdiff
path: root/contrib/run-script-casc26-tfa
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-06-21 10:24:11 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-06-21 10:24:39 -0500
commitcdf019f8be3b4affdb582ceb95054b327006521c (patch)
tree48f7091d06d1eea5abe9f4773b26a18a0bf7c8fa /contrib/run-script-casc26-tfa
parent89e41ba0f27c6f2c8aceb1884df7392a6ef577c7 (diff)
Update casc and sygus comp scripts.
Diffstat (limited to 'contrib/run-script-casc26-tfa')
-rw-r--r--contrib/run-script-casc26-tfa12
1 files changed, 5 insertions, 7 deletions
diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa
index 9f6749ed6..aa65a938f 100644
--- a/contrib/run-script-casc26-tfa
+++ b/contrib/run-script-casc26-tfa
@@ -7,7 +7,7 @@ bench="$1"
file=${bench##*/}
filename=${file%.*}
-echo "------- cvc4-tfa casc j8 : $bench at $2..."
+echo "------- cvc4-tfa casc 26 : $bench at $2..."
# use: trywith [params..]
# to attempt a run. If an SZS ontology result is printed, then
@@ -31,11 +31,9 @@ function finishwith {
trywith 10 --decision=internal --full-saturate-quant
trywith 10 --finite-model-find --decision=internal
-trywith 10 --nl-ext --nl-ext-tplanes --decision=internal --full-saturate-quant
-trywith 10 --purify-quant --full-saturate-quant
+trywith 10 --nl-ext --nl-ext-tplanes --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 30 --nl-ext --fs-inst --full-saturate-quant
-finishwith --nl-ext --nl-ext-tplanes --full-saturate-quant
+trywith 15 --cbqi-all --purify-triggers --full-saturate-quant
+trywith 15 --nl-ext --fs-inst --full-saturate-quant
+finishwith --full-saturate-quant --macros-quant
# echo "% SZS status" "GaveUp for $filename"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback