diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 9023d38298d..5e6e03b7f03 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1743,7 +1743,7 @@ seq_util::rex::info seq_util::rex::info::star() const { seq_util::rex::info seq_util::rex::info::plus() const { if (is_known()) { //r+ is not normalized if r is nullable, the normalized form would be r* - info(classical, classical, interpreted, nonbranching, (nullable == l_false ? normalized : false), monadic, false, nullable, min_length, star_height + 1); + return info(classical, classical, interpreted, nonbranching, (nullable == l_false ? normalized : false), monadic, false, nullable, min_length, star_height + 1); } else return *this; @@ -1791,7 +1791,7 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info & rhs, bool seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info& rhs) const { if (is_known() || rhs.is_known()) { //works correctly if one of the arguments is unknown - info(classical & rhs.classical, + return info(classical & rhs.classical, standard && rhs.standard, interpreted && rhs.interpreted, nonbranching && rhs.nonbranching, @@ -1830,7 +1830,7 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info& rhs) const { seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info& rhs) const { if (is_known()) { if (rhs.is_known()) { - info(false, + return info(false, standard & rhs.standard, interpreted & rhs.interpreted, nonbranching & rhs.nonbranching, diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 86655b55717..dd144530e65 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -479,13 +479,13 @@ class seq_util { info star() const; info plus() const; info opt() const; + info compl() const; info concat(info & rhs, bool lhs_is_concat) const; info disj(info& rhs) const; info conj(info& rhs) const; info diff(info& rhs) const; info orelse(info& rhs) const; info loop(unsigned lower) const; - info compl() const; }; private: seq_util& u;