added missing return statements, reordered def of compl to match decl…

…aration order of methods
Z3Prover · Aug 21, 2020 · 3fb226d · 3fb226d
1 parent 1099c51
commit 3fb226d
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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;