diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-03 13:27:52 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-03 13:27:52 -0500 |
| commit | b4e5b3250f6aaa82525aa7f5afa8de3086e2c5ee (patch) | |
| tree | 8e13b087ff1ddd41ff65fa8073693dca0f00bba5 /contrib/run-script-smtcomp2017 | |
| parent | 92f56a7ba4f4f7a79761829f9c8b67929c8503ee (diff) | |
Minor to smt comp script.
Diffstat (limited to 'contrib/run-script-smtcomp2017')
| -rw-r--r-- | contrib/run-script-smtcomp2017 | 3 |
1 files changed, 3 insertions, 0 deletions
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) |