diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
| commit | 3ce21ef9a8b6daa1eef1dbe9af10a84e8c87e413 (patch) | |
| tree | 2686fa03573e19593e3395d4097ce1e7943ba04a /contrib | |
| parent | e7439fc0daf1049f59540b9aeb890a52d86a77bd (diff) | |
Avoid ensureLiteral on unpreprocessed formulas in cbqi.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2015 | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index 831c892be..c66ee11c6 100644 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -67,12 +67,11 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 20 --enable-cbqi --full-saturate-quant + trywith 20 --cbqi --full-saturate-quant trywith 20 --full-saturate-quant - trywith 20 --cbqi-recurse --full-saturate-quant - trywith 30 --quant-cf --full-saturate-quant - trywith 60 --quant-cf --qcf-tconstraint --full-saturate-quant - trywith 120 --cbqi-recurse --disable-prenex-quant --full-saturate-quant + trywith 20 --cbqi --cbqi-recurse --full-saturate-quant + trywith 60 --qcf-tconstraint --full-saturate-quant + trywith 120 --cbqi --cbqi-recurse --full-saturate-quant finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant ;; QF_AUFBV) |