From 22b9203dea06e729bb734cde63eece0f1133f884 Mon Sep 17 00:00:00 2001
From: Zvonimir Rakamaric <zvonimir@cs.utah.edu>
Date: Mon, 28 Feb 2022 21:37:20 -0700
Subject: [PATCH] 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 | 12 ------------
 share/smack/top.py          | 25 ++++++++++++++++++++++---
 2 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 188a4ae43..1650922bb 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -69,13 +69,6 @@ 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"
@@ -83,11 +76,6 @@ def verify_bpl_svcomp(args):
   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
diff --git a/share/smack/top.py b/share/smack/top.py
index d2fa3863b..1e3a51e54 100644
--- a/share/smack/top.py
+++ b/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)