Fix svcomp assert (#779)

Moved replacement of error_reach with assert false into preprocessing

We needed this so that we can run SVCOMP benchmarks without
setting verifier option to SVCOMP.

share/smack/svcomp/utils.py

@@ -69,25 +69,13 @@ def force_timeout():
   sys.stdout.flush()
   time.sleep(1000)
 
-def inject_assert_false(args):
-  with open(args.bpl_file, 'r') as bf:
-    content = bf.read()
-  content = content.replace('call reach_error();', 'assert false; call reach_error();')
-  with open(args.bpl_file, 'w') as bf:
-    bf.write(content)
-
 def verify_bpl_svcomp(args):
   """Verify the Boogie source file using SVCOMP-tuned heuristics."""
   heurTrace = "\n\nHeuristics Info:\n"
 
   from smack.top import VProperty
   from smack.top import VResult
 
-  if not (VProperty.MEMORY_SAFETY in args.check
-          or VProperty.MEMLEAK in args.check
-          or VProperty.INTEGER_OVERFLOW in args.check):
-    inject_assert_false(args)
-
   # Setting good loop unroll bound based on benchmark class
   loopUnrollBar = 13
   time_limit = 880

share/smack/top.py

@@ -777,6 +777,7 @@ def llvm_to_bpl(args):
     try_command(cmd, console=True)
     annotate_bpl(args)
     memsafety_subproperty_selection(args)
+    replace_reach_error(args)
     transform_bpl(args)
 
 
@@ -841,6 +842,25 @@ def replace_assertion(m):
             f.write(line)
 
 
+def replace_reach_error(args):
+    """Replaces calls to reach_error in SVCOMP benchmarks with assert false."""
+
+    if args.language != 'svcomp':
+        return
+
+    if (VProperty.MEMORY_SAFETY in args.check or
+            VProperty.MEMLEAK in args.check or
+            VProperty.INTEGER_OVERFLOW in args.check):
+        return
+
+    with open(args.bpl_file, 'r') as bf:
+        content = bf.read()
+    content = content.replace('call reach_error();',
+                              'assert false; call reach_error();')
+    with open(args.bpl_file, 'w') as bf:
+        bf.write(content)
+
+
 def transform_bpl(args):
     if args.transform_bpl:
         with open(args.bpl_file, 'r+') as bpl:
@@ -991,9 +1011,8 @@ def verify_bpl(args):
 
     elif args.verifier == 'corral':
         command = corral_command(args)
-        args.verifier_options += (
-            " /bopt:proverOpt:O:smt.qi.eager_threshold=100"
-            " /bopt:proverOpt:O:smt.arith.solver=2")
+        command += ["/bopt:proverOpt:O:smt.qi.eager_threshold=100"]
+        command += ["/bopt:proverOpt:O:smt.arith.solver=2"]
 
     elif args.verifier == 'symbooglix':
         command = symbooglix_command(args)