From 475267ac254f6f5ec2202b58c26d8ea82c9d2e4a Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 2 Aug 2022 17:04:34 +0200
Subject: smtbmc: Add --check-witness mode

This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
---
 backends/smt2/smtbmc.py | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

(limited to 'backends/smt2/smtbmc.py')

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index b8ea22aaf..3714e2918 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -54,6 +54,7 @@ smtctop = None
 noinit = False
 binarymode = False
 keep_going = False
+check_witness = False
 so = SmtOpts()
 
 
@@ -170,6 +171,10 @@ def usage():
         covering all found failed assertions, the character '%' is
         replaced in all dump filenames with an increasing number.
 
+    --check-witness
+        check that the used witness file contains sufficient
+        constraints to force an assertion failure.
+
 """ + so.helpmsg())
     sys.exit(1)
 
@@ -178,7 +183,7 @@ try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
              "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
-             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
+             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
 except:
     usage()
 
@@ -257,6 +262,8 @@ for o, a in opts:
         binarymode = True
     elif o == "--keep-going":
         keep_going = True
+    elif o == "--check-witness":
+        check_witness = True
     elif so.handle(o, a):
         pass
     else:
@@ -1774,6 +1781,7 @@ else:  # not tempind, covermode
 
                         smt_assert("(not %s)" % active_assert_expr)
                     else:
+                        active_assert_expr = "true"
                         smt_assert("false")
 
 
@@ -1781,6 +1789,17 @@ else:  # not tempind, covermode
                         if retstatus != "FAILED":
                             print("%s BMC failed!" % smt.timestamp())
 
+                        if check_witness:
+                            print_msg("Checking witness constraints...")
+                            smt_pop()
+                            smt_push()
+                            smt_assert(active_assert_expr)
+                            if smt_check_sat() != "sat":
+                                retstatus = "PASSED"
+                                check_witness = False
+                                num_steps = -1
+                                break
+
                         if append_steps > 0:
                             for i in range(last_check_step+1, last_check_step+1+append_steps):
                                 print_msg("Appending additional step %d." % i)
@@ -1873,6 +1892,8 @@ else:  # not tempind, covermode
         print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
+    if check_witness:
+        retstatus = "FAILED"
 
 smt.write("(exit)")
 smt.wait()
-- 
cgit v1.2.3