From c0ed683882c77143539050149cb1e6ef27cbd735 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 17 Jan 2018 13:32:44 -0500
Subject: [PATCH] disable regex length constraint generation as it currently
 makes unsound axioms

---
 src/smt/theory_str.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3dccc5681..9aec6fab7 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9609,6 +9609,8 @@ namespace smt {
                     continue;
                 }
 
+                // DISABLED due to bug -- star-over-union (and possibly others) results in unsound constraints
+                /*
                 if (!regex_terms_with_length_constraints.contains(str_in_re)) {
                     if (current_assignment == l_true && check_regex_length_linearity(re)) {
                         TRACE("str", tout << "regex length constraints expected to be linear -- generating and asserting them" << std::endl;);
@@ -9654,6 +9656,7 @@ namespace smt {
                         regex_axiom_add = true;
                     }
                 } // re not in regex_terms_with_length_constraints
+                */
 
                 rational exact_length_value;
                 if (get_len_value(str, exact_length_value)) {