From 0c2c1861f18082a5a6bcdb7cec3f42a1327d61f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 May 2020 20:50:18 -0700 Subject: [PATCH] add general purpose emptiness/non-emptiness check Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 900092c98..4b2db66f8 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -280,8 +280,8 @@ namespace smt { VERIFY(u().is_re(r, seq_sort)); expr_ref emp(re().mk_empty(seq_sort), m); literal lit = ~th.mk_eq(r, emp, false); - expr_ref is_non_empty = sk().mk_is_non_empty(r, emp); - th.add_axiom(~lit, th.mk_literal(is_non_empty)); + expr_ref is_empty = sk().mk_is_empty(r, emp); + th.add_axiom(~lit, th.mk_literal(is_empty)); } void seq_regex::propagate_ne(expr* r1, expr* r2) { @@ -297,8 +297,8 @@ namespace smt { VERIFY(u().is_re(r, seq_sort)); expr_ref emp(re().mk_empty(seq_sort), m); literal lit = ~th.mk_eq(r, emp, false); - expr_ref is_empty = sk().mk_is_empty(r, emp); - th.add_axiom(~lit, th.mk_literal(is_empty)); + expr_ref is_non_empty = sk().mk_is_non_empty(r, emp); + th.add_axiom(~lit, th.mk_literal(is_non_empty)); } bool seq_regex::is_member(expr* r, expr* u) {