From f1f79835adeac5c22fb744c38a83fef01d0002ad Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 11 Jun 2015 15:03:52 +0200 Subject: Update experimental scripts. Support top-level non-terminals in sygus grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression. --- contrib/run-script-smtcomp2015-application-experimental | 2 +- contrib/run-script-smtcomp2015-experimental | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) (limited to 'contrib') 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 -- cgit v1.2.3