diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 15:03:52 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-11 15:03:52 +0200 |
| commit | f1f79835adeac5c22fb744c38a83fef01d0002ad (patch) | |
| tree | d6f69c1426ee36f8aeba5fbd0a92a008c4f68d7f /contrib | |
| parent | 5ad9f1e8a19d9658a86203fe2db8ad9fb329cd8e (diff) | |
Update experimental scripts. Support top-level non-terminals in sygus grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2015-application-experimental | 2 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2015-experimental | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2015-application-experimental b/contrib/run-script-smtcomp2015-application-experimental index dac870c75..81d05c774 100755 --- a/contrib/run-script-smtcomp2015-application-experimental +++ b/contrib/run-script-smtcomp2015-application-experimental @@ -36,7 +36,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) runcvc4 --incremental ;; LIA|LRA|NIA|NRA) - runcvc4 --incremental --cbqi + runcvc4 --incremental --cbqi2 ;; QF_BV) runcvc4 --incremental --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 diff --git a/contrib/run-script-smtcomp2015-experimental b/contrib/run-script-smtcomp2015-experimental index 8aee209e0..02766943f 100755 --- a/contrib/run-script-smtcomp2015-experimental +++ b/contrib/run-script-smtcomp2015-experimental @@ -67,10 +67,14 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 180 --cbqi --full-saturate-quant + trywith 240 --cbqi2 --full-saturate-quant trywith 60 --full-saturate-quant + trywith 180 --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --cbqi2 --decision=internal --full-saturate-quant trywith 180 --qcf-tconstraint --full-saturate-quant - finishwith --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --cbqi --decision=internal --full-saturate-quant + trywith 180 --cbqi --full-saturate-quant + finishwith --cbqi2 --cbqi-recurse --full-saturate-quant ;; QF_AUFBV) trywith 600 |