diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-21 10:24:11 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-21 10:24:39 -0500 |
commit | cdf019f8be3b4affdb582ceb95054b327006521c (patch) | |
tree | 48f7091d06d1eea5abe9f4773b26a18a0bf7c8fa /contrib/run-script-casc26-tfa | |
parent | 89e41ba0f27c6f2c8aceb1884df7392a6ef577c7 (diff) |
Update casc and sygus comp scripts.
Diffstat (limited to 'contrib/run-script-casc26-tfa')
-rw-r--r-- | contrib/run-script-casc26-tfa | 12 |
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" |