From 7a93e2296de380354171fe4aab8bfc1b7c5e46c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2026 09:38:37 -0700 Subject: [PATCH] coding nit Signed-off-by: Nikolaj Bjorner --- src/smt/theory_nseq.cpp | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index b17856365..8e59e847c 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -177,15 +177,13 @@ namespace smt { void theory_nseq::new_diseq_eh(theory_var v1, theory_var v2) { expr* e1 = get_enode(v1)->get_expr(); expr* e2 = get_enode(v2)->get_expr(); - if (m_seq.is_re(e1)) { + if (m_seq.is_re(e1)) // regex disequality: nseq cannot verify language non-equivalence push_unhandled_pred(); - return; - } - if (!m_seq.is_seq(e1)) - return; - - m_axioms.diseq_axiom(e1, e2); + else if (m_seq.is_seq(e1)) + m_axioms.diseq_axiom(e1, e2); + else + ; } // -----------------------------------------------------------------------