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 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/run-script-smtcomp2015-application-experimental') 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 -- cgit v1.2.3