diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index 525f6b3db..477874bc0 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -92,6 +92,7 @@ namespace smt { void add_unit_axiom(expr* n) { m_ax.unit_axiom(n); } void add_length_axiom(expr* n) { m_ax.length_axiom(n); } void unroll_not_contains(expr* n) { m_ax.unroll_not_contains(n); } + void not_contains_axiom(expr* n) { m_ax.not_contains_axiom(n); } literal is_digit(expr* ch) { return mk_literal(m_ax.is_digit(ch)); } expr_ref add_length_limit(expr* s, unsigned k) { return m_ax.length_limit(s, k); } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index c73eec720..d09842ab7 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -246,7 +246,7 @@ namespace smt { if (is_true) m_axioms.contains_true_axiom(e); else - m_axioms.unroll_not_contains(e); + m_axioms.not_contains_axiom(e); } else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) { // axioms added via relevant_eh → dequeue_axiom