Skip to content

Commit 7596217

Browse files
fix #2481
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent 9fa9aa0 commit 7596217

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/smt/theory_seq.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5541,6 +5541,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
55415541
else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
55425542
// no-op
55435543
}
5544+
else if (m_util.is_skolem(e)) {
5545+
// no-op
5546+
}
55445547
else {
55455548
TRACE("seq", tout << mk_pp(e, m) << "\n";);
55465549
UNREACHABLE();

0 commit comments

Comments
 (0)