fix #6178

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 21, 2022 · 1b83a45 · 1b83a45
1 parent 5b219aa
commit 1b83a45
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -3070,9 +3070,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     }
     else if (m_util.str.is_is_digit(e)) {
 
+    }
+    else if (m_util.str.is_foldl(e) || m_util.str.is_foldli(e)) {
+
     }
     else {
         TRACE("seq", tout << mk_pp(e, m) << "\n";);
+        IF_VERBOSE(0, verbose_stream() << mk_pp(e, m) << "\n");
         UNREACHABLE();
     }
 }