diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-09 11:45:14 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-09 11:45:14 +0200 |
| commit | 3fbe87912dbffe70cf01fdf0b4652960998ea480 (patch) | |
| tree | 252c48277f8d2946823d80610c2065148fc8422e /contrib | |
| parent | 591649f4631e348b65b61d3f1f4ccfe1f6baf7cc (diff) | |
Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization for non-UF logics. Update SMT COMP scripts accordingly.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2015 | 8 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-assertions | 4 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-experimental | 6 |
3 files changed, 6 insertions, 12 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index c46671c08..8eb19a24f 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -54,7 +54,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality trywith 30 --inst-when=full --full-saturate-quant - trywith 30 --fmf-bound-int --macros-quant + #trywith 30 --fmf-bound-int --macros-quant # recently bug fixed trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --decision=justification-stoponly --full-saturate-quant # large runs 3min @@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 60 --cbqi --no-cbqi-sat --full-saturate-quant + trywith 180 --cbqi --no-cbqi-sat --full-saturate-quant trywith 60 --full-saturate-quant - trywith 60 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - trywith 240 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant - finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 diff --git a/contrib/run-script-smtcomp2015-assertions b/contrib/run-script-smtcomp2015-assertions index 3292e29fb..c4f9fc6cc 100755 --- a/contrib/run-script-smtcomp2015-assertions +++ b/contrib/run-script-smtcomp2015-assertions @@ -74,10 +74,8 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) LIA|LRA|NIA|NRA) trywith 30 --cbqi --no-cbqi-sat --full-saturate-quant trywith 30 --full-saturate-quant - trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant trywith 30 --qcf-tconstraint --full-saturate-quant - trywith 30 --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant - finishwith --cbqi --no-cbqi-sat --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --no-cbqi-sat --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 30 diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental index 9b8a0ba38..3480a8e3c 100755 --- a/contrib/run-script-smtcomp2015-experimental +++ b/contrib/run-script-smtcomp2015-experimental @@ -67,12 +67,10 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 60 --cbqi --full-saturate-quant + trywith 180 --cbqi --full-saturate-quant trywith 60 --full-saturate-quant - trywith 60 --cbqi --cbqi-recurse --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - trywith 240 --cbqi --cbqi-recurse --full-saturate-quant - finishwith --cbqi --cbqi-recurse --pre-skolem-quant --full-saturate-quant + finishwith --cbqi --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 |