diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:02:51 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:03:20 -0500 |
| commit | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (patch) | |
| tree | ebe6334ca8a415a4d5a24a83ee40441419c93876 /contrib | |
| parent | ae1d4e4f05fdc2db61d7de7efee5bd567363ceef (diff) | |
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-casc26-fnt | 2 | ||||
| -rw-r--r-- | contrib/run-script-casc26-fof | 8 | ||||
| -rw-r--r-- | contrib/run-script-casc26-tfa | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/contrib/run-script-casc26-fnt b/contrib/run-script-casc26-fnt index c3c12f937..c89d3eb0a 100644 --- a/contrib/run-script-casc26-fnt +++ b/contrib/run-script-casc26-fnt @@ -33,5 +33,5 @@ function finishwith { 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 +finishwith --finite-model-find --macros-quant --macros-quant-mode=all --sort-inference --uf-ss-fair # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-fof b/contrib/run-script-casc26-fof index 376d18b15..5ec312cb7 100644 --- a/contrib/run-script-casc26-fof +++ b/contrib/run-script-casc26-fof @@ -34,7 +34,7 @@ function finishwith { # 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 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 @@ -43,8 +43,8 @@ trywith 15 --prenex-quant=none --full-saturate-quant trywith 15 --fs-inst --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 --full-saturate-quant --macros-quant -trywith 30 --fs-inst --full-saturate-quant +trywith 30 --decision=internal --full-saturate-quant +trywith 30 --qcf-vo-exp --full-saturate-quant trywith 30 --no-quant-cf --full-saturate-quant -finishwith --qcf-vo-exp --full-saturate-quant +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa index aa65a938f..05062bf5c 100644 --- a/contrib/run-script-casc26-tfa +++ b/contrib/run-script-casc26-tfa @@ -31,9 +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 --full-saturate-quant +trywith 10 --multi-trigger-when-single --multi-trigger-priority --nl-ext --nl-ext-tplanes --full-saturate-quant trywith 10 --partial-triggers --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 +finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" |