Abort when sygus-verify finds unsoundness. (#1717)

2 files changed, 15 insertions, 0 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 1437e9992..c40491a40 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1123,6 +1123,14 @@ header = "options/quantifiers_options.h"
   help       = "use sygus to verify the correctness of rewrite rules via sampling"
 
 [[option]]
+  name       = "sygusRewVerifyAbort"
+  category   = "regular"
+  long       = "sygus-rr-verify-abort"
+  type       = "bool"
+  default    = "true"
+  help       = "abort when sygus-rr-verify finds an instance of unsoundness"
+
+[[option]]
   name       = "sygusSamples"
   category   = "regular"
   long       = "sygus-samples=N"
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 7fe403526..4d3584596 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -827,9 +827,16 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
             }
             else
             {
+              // no witness point found?
               Assert(false);
             }
           }
+          if (options::sygusRewVerifyAbort())
+          {
+            AlwaysAssert(
+                false,
+                "--sygus-rr-verify detected unsoundness in the rewriter!");
+          }
         }
       }