diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 93b4be173..81f1af06f 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -117,6 +117,7 @@ namespace smt { } if (u.is_seq(s, ch)) { expr* v = m_model.get_fresh_value(ch); + if (!v) return nullptr; return u.str.mk_unit(v); } UNREACHABLE();