projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
b66afc0
)
Disable sort inference for SMT COMP
author
ajreynol
<andrew.j.reynolds@gmail.com>
Sat, 13 Jun 2015 21:05:26 +0000
(23:05 +0200)
committer
ajreynol
<andrew.j.reynolds@gmail.com>
Sat, 13 Jun 2015 21:05:26 +0000
(23:05 +0200)
contrib/run-script-smtcomp2015
patch
|
blob
|
history
diff --git
a/contrib/run-script-smtcomp2015
b/contrib/run-script-smtcomp2015
index 6e099f3afddd86135c2d0ca9ee23dbe5779e6b6a..2dac38935fbb611834a77fec7604d2fd880ae4e7 100755
(executable)
--- a/
contrib/run-script-smtcomp2015
+++ b/
contrib/run-script-smtcomp2015
@@
-48,7
+48,7
@@
ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
trywith 10 --qcf-tconstraint --full-saturate-quant
# medium runs 5min
trywith 30 --no-quant-cf --full-saturate-quant
trywith 10 --qcf-tconstraint --full-saturate-quant
# medium runs 5min
trywith 30 --no-quant-cf --full-saturate-quant
- trywith 30 --finite-model-find --fmf-inst-engine --
sort-inference --uf-ss-fair --
mbqi=gen-ev
+ trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
trywith 30 --pre-skolem-quant --full-saturate-quant
trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant
trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant
trywith 30 --pre-skolem-quant --full-saturate-quant
trywith 30 --no-inst-no-entail --no-quant-cf --full-saturate-quant
@@
-62,7
+62,7
@@
ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA)
trywith 60 --finite-model-find --mbqi=none
trywith 60 --decision=internal --full-saturate-quant
# last call runs 20min
trywith 60 --finite-model-find --mbqi=none
trywith 60 --decision=internal --full-saturate-quant
# last call runs 20min
- trywith 300 --finite-model-find --fmf-inst-engine --quant-cf
--sort-inference --uf-ss-fair
+ trywith 300 --finite-model-find --fmf-inst-engine --quant-cf
trywith 300 --no-inst-no-entail --full-saturate-quant
finishwith --full-saturate-quant
;;
trywith 300 --no-inst-no-entail --full-saturate-quant
finishwith --full-saturate-quant
;;