More missing changes from svcomp (#596)

* Remove old svcomp options * Add missing option to svcomp script --------- Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Dec 22, 2023 · e5c25c1 · e5c25c1
1 parent 6205e51
commit e5c25c1
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 5 deletions.
diff --git a/Dartagnan-SVCOMP.sh b/Dartagnan-SVCOMP.sh
@@ -25,14 +25,16 @@ else
 
     export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn"
 
+    skip_assertions_of_type="--program.processing.skipAssertionsOfType=USER"
     if [[ $propertypath == *"no-overflow.prp"* ]]; then
         export CFLAGS="-fgnu89-inline -fsanitize=signed-integer-overflow"
     elif [[ $propertypath == *"valid-memsafety.prp"* ]]; then
         export CFLAGS="-fgnu89-inline -fsanitize=null"
     else
         export CFLAGS="-fgnu89-inline"
+        skip_assertions_of_type=""
     fi
 
-    cmd="java -jar svcomp/target/svcomp.jar --method=assume --program.processing.constantPropagation=false --encoding.integers=true --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness
+    cmd="java -jar svcomp/target/svcomp.jar --method=assume --encoding.integers=true $skip_assertions_of_type --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness
     $cmd
 fi
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
@@ -65,9 +65,6 @@ public class OptionNames {
     public static final String UMIN = "svcomp.umin";
     public static final String UMAX = "svcomp.umax";
     public static final String STEP = "svcomp.step";
-    public static final String SANITIZE = "svcomp.sanitize";
-    public static final String OPTIMIZATION = "svcomp.optimization";
-    public static final String INTEGER_ENCODING = "svcomp.integerEncoding";
 
     // Debugging Options
     public static final String PRINT_PROGRAM_BEFORE_PROCESSING = "printer.beforeProcessing";

diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java
@@ -171,7 +171,7 @@ public static void main(String[] args) throws Exception {
     private static List<String> filterOptions(Configuration config) {
 
         // BOUND is computed based on umin and the information from the witness
-        List<String> skip = Arrays.asList(PROPERTYPATH, UMIN, UMAX, STEP, SANITIZE, BOUND);
+        List<String> skip = Arrays.asList(PROPERTYPATH, UMIN, UMAX, STEP, BOUND);
 
         return Arrays.stream(config.asPropertiesString().split("\n")).
             filter(p -> skip.stream().noneMatch(s -> s.equals(p.split(" = ")[0]))).