diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-26 16:15:16 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-26 16:15:16 -0700 |
| commit | 44dfd74baea6b23a1a7538fa8f376e9ffafd5f15 (patch) | |
| tree | f2eb5459b77efdc1d5ba425e64db5153b5d7e474 /contrib | |
| parent | 06cfada2e6521fe0d58abccacfcd9fe42a43c86c (diff) | |
| parent | d133e87221b0de3a4eb7c286cebda14548874e7c (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/get-cryptominisat4 | 2 | ||||
| -rw-r--r-- | contrib/run-script-smtcomp2016 | 10 |
2 files changed, 9 insertions, 3 deletions
diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4 index a1a8cb786..c96bbe03d 100755 --- a/contrib/get-cryptominisat4 +++ b/contrib/get-cryptominisat4 @@ -47,7 +47,7 @@ patch -p0 < ../../contrib/cryptominisat-4.2.0.second.patch mkdir ../build cd ../build -cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" ../cryptominisat-$version +cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" -DNOM4RI="ON" ../cryptominisat-$version make install -j2 cd ../ diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016 index 0db378a80..ad036ad05 100644 --- a/contrib/run-script-smtcomp2016 +++ b/contrib/run-script-smtcomp2016 @@ -41,7 +41,7 @@ QF_NIA) trywith 1800 --solve-int-as-bv=16 --bitblast=eager finishwith --solve-int-as-bv=32 --bitblast=eager ;; -ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) # the following is designed for a run time of 2400s (40 min). # initial runs 1min trywith 20 --simplification=none --full-saturate-quant @@ -72,8 +72,14 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) # finish 12min finishwith --full-saturate-quant ;; +UFBV) + # many problems in UFBV are essentially BV + trywith 300 --full-saturate-quant + trywith 300 --finite-model-find + finishwith --cbqi-all --full-saturate-quant + ;; BV) - trywith 30 --finite-model-find + trywith 300 --finite-model-find finishwith --cbqi-all --full-saturate-quant ;; LIA|LRA|NIA|NRA) |