fix #4480

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · May 31, 2020 · 7d4c9e6 · 7d4c9e6
1 parent 084cd33
commit 7d4c9e6
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
@@ -3125,6 +3125,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.is_skolem(e)) {
 
         // no-op
+    }
+    else if (m_util.str.is_is_digit(e)) {
+
     }
     else {
         TRACE("seq", tout << mk_pp(e, m) << "\n";);