From 28b20948a3b236bf32ca399e2cd85b09c1e57e67 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 26 May 2016 14:51:01 -0500 Subject: Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf. --- contrib/run-script-smtcomp2016 | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'contrib') diff --git a/contrib/run-script-smtcomp2016 b/contrib/run-script-smtcomp2016 index 8ac8d5c1d..056cddb8e 100644 --- a/contrib/run-script-smtcomp2016 +++ b/contrib/run-script-smtcomp2016 @@ -33,7 +33,7 @@ QF_LIA) # same as QF_LRA but add --pb-rewrites finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites ;; -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 @@ -64,8 +64,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) -- cgit v1.2.3 From 5a97ae0820747af37f1cabce69e7649e88acb681 Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 26 May 2016 18:35:34 -0400 Subject: Disabled m4ri in cryptominisat cmake command --- contrib/get-cryptominisat4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib') 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 ../ -- cgit v1.2.3