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

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 1437e9992034b9165f8cf17cb33b2318677ec266..c40491a40d688c14ee1638dd6769adbc25ffb496 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1122,6 +1122,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   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"

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 7fe403526f48e2bfc893020e321cd5da1c093d08..4d35845968dcf1c677b61125c49f0f949fffeae1 100644 (file)
--- 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!");
+          }
         }
       }