From b4e5b3250f6aaa82525aa7f5afa8de3086e2c5ee Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 3 Jun 2017 13:27:52 -0500 Subject: [PATCH] Minor to smt comp script. --- contrib/run-script-smtcomp2017 | 3 +++ 1 file changed, 3 insertions(+) diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index ffa54bec9..9e351d58e 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -63,6 +63,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF trywith 30 --inst-when=full --full-saturate-quant trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant trywith 30 --nl-ext --full-saturate-quant + trywith 30 --full-saturate-quant --quant-ind trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant # finite model find 2min trywith 20 --finite-model-find --mbqi=none @@ -83,11 +84,13 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF UFBV) # most problems in UFBV are essentially BV trywith 300 --full-saturate-quant + trywith 300 --full-saturate-quant --no-cbqi trywith 300 --full-saturate-quant --cbqi --decision=internal finishwith --finite-model-find ;; BV) trywith 300 --full-saturate-quant + trywith 300 --full-saturate-quant --no-cbqi finishwith --full-saturate-quant --cbqi --decision=internal ;; LIA|LRA) -- 2.30.2