From 57460a8bd790453d6aa0637353ee426b0ab8503c Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Fri, 5 Nov 2021 13:21:31 +0100 Subject: [PATCH] Use assume solver for svcomp --- Dartagnan-SVCOMP.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Dartagnan-SVCOMP.sh b/Dartagnan-SVCOMP.sh index 463fc4cd7e..73e2c49e10 100755 --- a/Dartagnan-SVCOMP.sh +++ b/Dartagnan-SVCOMP.sh @@ -23,11 +23,11 @@ else export DAT3M_HOME=$(pwd) export PATH=$PATH:$DAT3M_HOME/smack/bin - FLAGS="-method incremental" + FLAGS="-method assume" if ! grep -q "pthread" $PROGRAMPATH; then FLAGS+=" -o O3 -e bit-vector -cat cat/sc.cat" else - FLAGS+=" -cat cat/svcomp.cat -step 5 -umax 27" + FLAGS+=" -step 5 -umax 27 -cat cat/svcomp.cat" fi cmd="java -jar svcomp/target/svcomp-"$VERSION".jar "$FLAGS" -property "$PROPERTYPATH" -i "$PROGRAMPATH" "$WITNESS