From 33cdc06eb49ba991d2b40f384b0383454b16f1b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 May 2020 13:37:49 -0700 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index b8d48c224..677baa4fb 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -299,7 +299,7 @@ namespace smt { } /** - nonempty(R union Q, Seen) = R = {} or Q = {} + nonempty(R union Q, Seen) = R != {} or Q != {} nonempty(R[if(p,R1,R2)], Seen) = if(p, nonempty(R[R1], Seen), nonempty(R[R2], Seen)) (co-factor) nonempty(R, Seen) = nullable(R) or (R not in Seen and nonempty(D(first(R),R), Seen u { R })) (derivative)