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/run-script-smtcomp2015-application-experimental | |
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/run-script-smtcomp2015-application-experimental')
-rwxr-xr-x | contrib/run-script-smtcomp2015-application-experimental | 2 |
1 files changed, 1 insertions, 1 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 |