mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

coding nit

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-19 09:38:37 -07:00
parent 2ec305f206
commit 7a93e2296d
1 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_nseq.cpp
View file

@ -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
;
}
// -----------------------------------------------------------------------