Merge branch 'master' into fix-re-range-symbolic-bound-iss5140-02ba1d29bf05d7ec

cmake/compiler_warnings.cmake

@@ -24,8 +24,9 @@ set(CLANG_ONLY_WARNINGS
   "-Wsuggest-override"
   "-Winconsistent-missing-override"
   "-Wno-missing-field-initializers"
-  "-Wcast-qual"  
+  "-Wcast-qual"
 )
+
 set(MSVC_WARNINGS "/W3")
 
 ################################################################################

src/api/api_algebraic.cpp

@@ -447,4 +447,4 @@ extern "C" {
         return _am.get_i(av);
         Z3_CATCH_RETURN(0);
     }
-};
+}

src/api/api_arith.cpp

@@ -235,4 +235,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_array.cpp

@@ -358,4 +358,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_ast.cpp

@@ -1547,4 +1547,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_ast_map.cpp

@@ -161,4 +161,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_ast_vector.cpp

@@ -135,4 +135,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_ast_vector.h

@@ -21,7 +21,7 @@ Revision History:
 
 namespace api {
     class context;
-};
+}
 
 struct Z3_ast_vector_ref : public api::object {
     ast_ref_vector  m_ast_vector;

src/api/api_bv.cpp

@@ -399,4 +399,4 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_CATCH_RETURN(0);
     }
 
-};
+}

src/api/api_config_params.cpp

@@ -121,4 +121,4 @@ extern "C" {
         Z3_CATCH;
     }
 
-};
+}

src/api/api_context.cpp

@@ -359,7 +359,7 @@ namespace api {
         return *(m_rcf_manager.get());
     }
 
-};
+}
 
 
 // ------------------------
@@ -531,4 +531,4 @@ extern "C" {
         Z3_CATCH;
     }
     
-};
+}

src/api/api_context.h

@@ -45,16 +45,16 @@ Revision History:
 
 namespace smtlib {
     class parser;
-};
+}
 
 namespace realclosure {
     class manager;
-};
+}
 
 namespace smt2 {
     class parser;
     void free_parser(parser*);
-};
+}
 
 namespace api {
        
@@ -267,7 +267,7 @@ namespace api {
         
     };
     
-};
+}
 
 inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
 #define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }

src/api/api_datalog.cpp

@@ -142,7 +142,7 @@ namespace api {
         void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
         void updt_params(params_ref const& p) { m_context.updt_params(p); }
     };         
-};
+}
 
 extern "C" {
     
@@ -705,4 +705,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_datalog.h

@@ -30,7 +30,7 @@ typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*co
 namespace api {
     class fixedpoint_context;
     class context;
-};
+}
 
 
 struct Z3_fixedpoint_ref : public api::object {

src/api/api_datatype.cpp

@@ -687,4 +687,4 @@ extern "C" {
     }
 
 
-};
+}

src/api/api_finite_set.cpp

@@ -184,4 +184,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_fpa.cpp

@@ -1337,4 +1337,4 @@ extern "C" {
         Z3_CATCH_RETURN(false);
     }
 
-};
+}

src/api/api_goal.cpp

@@ -213,4 +213,4 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-};
+}

src/api/api_model.cpp

@@ -448,4 +448,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_numeral.cpp

@@ -489,4 +489,4 @@ extern "C" {
     }
 #endif
 
-};
+}

src/api/api_opt.cpp

@@ -503,4 +503,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_params.cpp

@@ -212,4 +212,4 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-};
+}

src/api/api_pb.cpp

@@ -106,4 +106,4 @@ extern "C" {
     }
 
 
-};
+}

src/api/api_polynomial.cpp

@@ -80,4 +80,4 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
-};
+}

src/api/api_quant.cpp

@@ -583,5 +583,5 @@ extern "C" {
         return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
     }
 
-};
+}
 

src/api/api_rcf.cpp

@@ -437,4 +437,4 @@ extern "C" {
         return from_rcnumeral(rcfm(c).get_sign_condition_coefficient(to_rcnumeral(a), i, j));
         Z3_CATCH_RETURN(nullptr);
     }
-};
+}

src/api/api_seq.cpp

@@ -369,4 +369,4 @@ extern "C" {
     MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP);
 
 
-};
+}

src/api/api_solver.cpp

@@ -1218,4 +1218,4 @@ extern "C" {
 
 
 
-};
+}

src/api/api_special_relations.cpp

@@ -61,4 +61,4 @@ extern "C" {
 }
 
     MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC);
-};
+}

src/api/api_stats.cpp

@@ -133,4 +133,4 @@ extern "C" {
         return memory::get_allocation_size();
     }
 
-};
+}

src/api/api_tactic.cpp

@@ -669,4 +669,4 @@ extern "C" {
 
     
 
-};
+}

src/api/api_util.h

@@ -46,7 +46,7 @@ namespace api {
         void inc_ref();
         void dec_ref();
     };
-};
+}
 
 inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
 inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }

src/ast/arith_decl_plugin.h

@@ -24,7 +24,7 @@ class sexpr;
 namespace algebraic_numbers {
     class anum;
     class manager;
-};
+}
 
 enum arith_sort_kind {
     REAL_SORT,

src/ast/datatype_decl_plugin.h

@@ -171,7 +171,7 @@ namespace datatype {
             size* subst(obj_map<sort, size*>& S) override;
             sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
         };
-    };
+    }
 
     class def {
         ast_manager&            m;
@@ -465,7 +465,7 @@ namespace datatype {
         sort_ref mk_tuple_datatype(svector<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs);
     };
 
-};
+}
 
 typedef datatype::accessor accessor_decl;
 typedef datatype::constructor constructor_decl;

src/ast/dl_decl_plugin.cpp

@@ -648,7 +648,7 @@ namespace datalog {
             m_fid = m.mk_family_id(symbol("datalog_relation"));
         }
         return m_fid;
-    };
+    }
 
     arith_util& dl_decl_util::arith() const {
         if (!m_arith) m_arith = alloc(arith_util, m);
@@ -788,4 +788,4 @@ namespace datalog {
         return m.mk_app(f, num_args, args);
     }
 
-};
+}

src/ast/dl_decl_plugin.h

@@ -199,5 +199,5 @@ namespace datalog {
 
     };
     
-};
+}
 

src/ast/euf/euf_ac_plugin.h

@@ -319,14 +319,14 @@ namespace euf {
 
         struct eq_pp {
             ac_plugin const& p; eq const& e; 
-            eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {}; 
+            eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {} 
             eq_pp(ac_plugin const& p, unsigned eq_id): p(p), e(p.m_active[eq_id]) {}
             std::ostream& display(std::ostream& out) const { return p.display_equation(out, e); }
         };
 
         struct eq_pp_ll {
             ac_plugin const& p; eq const& e;
-            eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {};
+            eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {}
             eq_pp_ll(ac_plugin const& p, unsigned eq_id) : p(p), e(p.m_active[eq_id]) {}
             std::ostream& display(std::ostream& out) const { return p.display_equation_ll(out, e); }
         };

src/ast/euf/euf_etable.cpp

@@ -276,5 +276,5 @@ namespace euf {
         return find(n) == n;
     }
 
-};
+}
 

src/ast/euf/euf_etable.h

@@ -179,7 +179,7 @@ namespace euf {
 
     };
 
-};
+}
 
 
 

src/ast/euf/euf_mam.h

@@ -81,5 +81,5 @@ namespace euf {
         static void ground_subterms(expr* e, ptr_vector<app>& ground);
 
     };
-};
+}
 

src/ast/euf/euf_plugin.h

@@ -47,7 +47,7 @@ namespace euf {
         
         virtual void merge_eh(enode* n1, enode* n2) = 0;
 
-        virtual void diseq_eh(enode* eq) {};
+        virtual void diseq_eh(enode* eq) {}
 
         virtual void propagate() = 0;
 

src/ast/for_each_expr.cpp

@@ -94,7 +94,7 @@ namespace has_skolem_functions_ns {
         void operator()(app const * n) const { if (n->get_decl()->is_skolem() && n->get_num_args() > 0) throw found(); }
         void operator()(quantifier * n) const {}
     };
-};
+}
 
 bool has_skolem_functions(expr * n) {
     has_skolem_functions_ns::proc p;

src/ast/format.cpp

@@ -195,4 +195,4 @@ namespace format_ns {
         return fm(m).mk_app(fid(m), OP_NIL);
     }
 
-};
+}

src/ast/format.h

@@ -198,6 +198,6 @@ namespace format_ns {
         return mk_seq4(m, begin, end, proc, static_cast<unsigned>(strlen(lp)), lp, rp);
     }
   
-};
+}
 
 

src/ast/fpa/fpa2bv_converter.h

@@ -162,10 +162,10 @@ public:
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;
 
-    special_t const & get_min_max_specials() const { return m_min_max_ufs; };
+    special_t const & get_min_max_specials() const { return m_min_max_ufs; }
-    const2bv_t const & get_const2bv() const { return m_const2bv; };
+    const2bv_t const & get_const2bv() const { return m_const2bv; }
-    const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; };
+    const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }
-    uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; };
+    uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; }
 
 protected:
     void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);

src/ast/macros/macro_manager.cpp

@@ -167,7 +167,7 @@ namespace macro_manager_ns {
             }
         }
     };
-};
+}
 
 /**
    \brief Mark all func_decls used in exprs as forbidden.

src/ast/macros/quasi_macros.cpp

@@ -71,7 +71,7 @@ void quasi_macros::find_occurrences(expr * e) {
             default: UNREACHABLE();
         }
     }
-};
+}
 
 bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
     return is_non_ground(e) && is_uninterp(e);

src/ast/polymorphism_inst.h

@@ -58,7 +58,7 @@ namespace polymorphism {
             void undo() override {
                 i.m_in_decl_queue.mark(i.m_decl_queue.back(), false);
                 i.m_decl_queue.pop_back();
-            };
+            }
         };
 
         struct remove_back : public trail {

src/ast/quantifier_stat.cpp

@@ -115,5 +115,5 @@ namespace q {
         return r;
     }
 
-};
+}
 

src/ast/quantifier_stat.h

@@ -149,6 +149,6 @@ namespace q {
         quantifier_stat * operator()(quantifier * q, unsigned generation);
     };
 
-};
+}
 
 

src/ast/recfun_decl_plugin.h

@@ -60,7 +60,7 @@ namespace recfun {
         func_decl_ref       m_pred; //<! predicate used for this case
         expr_ref_vector     m_guards; //<! conjunction that is equivalent to this case
         expr_ref            m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
-        def *               m_def = nullptr;; //<! definition this is a part of
+        def *               m_def = nullptr; //<! definition this is a part of
         bool                m_immediate = false; //<! does `rhs` contain no defined_fun/case_pred?
 
         case_def(ast_manager& m):
@@ -92,7 +92,7 @@ namespace recfun {
         expr * get_guard(unsigned i) const { return m_guards[i]; }
         expr * get_rhs() const { return m_rhs; }
         unsigned num_guards() const { return m_guards.size(); }
-        bool is_immediate() const { return m_immediate; };
+        bool is_immediate() const { return m_immediate; }
         void set_is_immediate(bool b) { m_immediate = b; }
     };
 

src/ast/rewriter/bv_bounds.h

@@ -34,7 +34,7 @@ public:
     typedef rational numeral;
     typedef std::pair<numeral, numeral> interval;
     typedef obj_map<app, numeral>       bound_map;
-    bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {};
+    bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {}
     ~bv_bounds();
 public: // bounds addition methods
     br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result);

src/ast/rewriter/seq_axioms.h

@@ -123,5 +123,5 @@ namespace seq {
 
     };
 
-};
+}
 

src/ast/rewriter/seq_eq_solver.cpp

@@ -727,5 +727,5 @@ namespace seq {
 
 
 
-};
+}
 

src/ast/rewriter/seq_eq_solver.h

@@ -167,5 +167,5 @@ namespace seq {
         
     };
 
-};
+}
 

src/ast/rewriter/seq_rewriter.cpp

@@ -3263,6 +3263,39 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         return BR_DONE;
     }
 
+    // (str.in_re e (re.range lo hi)) where a bound is not a concrete character.
+    // By SMT-LIB semantics (re.range lo hi) is the set of single characters c
+    // with lo <= c <= hi when lo and hi are themselves single characters, and
+    // the empty language otherwise; so membership is equivalent to lo, hi and
+    // e all being single characters with lo <= e <= hi.  The derivative engine
+    // only unfolds ranges whose bounds are concrete characters, so without this
+    // reduction a range with a symbolic bound is left unsolved (and mk_re_range
+    // deliberately keeps such a range symbolic rather than unsoundly collapsing
+    // it to re.empty).  Ranges with two concrete single-character bounds keep
+    // their existing derivative-based handling.
+    {
+        expr* rlo = nullptr, *rhi = nullptr;
+        if (re().is_range(b, rlo, rhi)) {
+            auto concrete_char = [&](expr* e) {
+                zstring s;
+                expr* ch = nullptr;
+                unsigned uc = 0;
+                return (str().is_string(e, s) && s.length() == 1) ||
+                       (str().is_unit(e, ch) && m_util.is_const_char(ch, uc));
+            };
+            if (!concrete_char(rlo) || !concrete_char(rhi)) {
+                expr_ref_vector conj(m());
+                conj.push_back(m().mk_eq(str().mk_length(rlo), one()));
+                conj.push_back(m().mk_eq(str().mk_length(rhi), one()));
+                conj.push_back(m().mk_eq(str().mk_length(a), one()));
+                conj.push_back(str().mk_lex_le(rlo, a));
+                conj.push_back(str().mk_lex_le(a, rhi));
+                result = m().mk_and(conj);
+                return BR_REWRITE_FULL;
+            }
+        }
+    }
+
     zstring s;
     if (str().is_string(a, s) && re().is_ground(b)) {
         // Just check membership and replace by true/false
@@ -4149,14 +4182,20 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
         else
             return BR_FAILED;
     }
+    else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
+        has_clo = true;
+    if (str().is_string(hi, shi) && shi.length() == 1) {
+        chi = shi[0];
+        has_chi = true;
+    }
+    else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
+        has_chi = true;
 
-    // clo/chi are only meaningful once both bounds were extracted; an early
+    if (!has_clo || !has_chi)
-    // is_empty (from the length checks) leaves them at their default 0, so the
+        return BR_FAILED;
-    // is_empty return must come before the singleton/ordering checks below.
-    if (!is_empty && clo > chi)
-        is_empty = true;
 
-    if (is_empty) {
+    // Both bounds are concrete characters: an inverted range is empty.
+    if (clo > chi) {
         sort* srt = re().mk_re(lo->get_sort());
         result = re().mk_empty(srt);
         return BR_DONE;

src/ast/rewriter/seq_skolem.h

@@ -171,5 +171,5 @@ namespace seq {
 
     };
 
-};
+}
 

src/ast/simplifiers/distribute_forall.cpp

@@ -101,5 +101,5 @@ void distribute_forall_simplifier::reduce() {
         if (r != d.fml())
             m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
     }
-};
+}
 

src/ast/simplifiers/propagate_values.cpp

@@ -62,7 +62,7 @@ void propagate_values::add_sub(dependent_expr const& de) {
         else if (m.is_value(y) && m_shared.is_shared(x))
             m_subst.insert(x, y, dep);
     }
-};
+}
 
 void propagate_values::reduce() {
     m_shared.reset();

src/ast/sls/sls_array_plugin.h

@@ -36,7 +36,7 @@ namespace sls {
                 for (unsigned i = 1; i < a.sel->num_args(); ++i)
                     h ^= a.sel->get_arg(i)->get_root()->hash();
                 return h;
-            };
+            }
         };
         struct select_args_eq {
             bool operator()(select_args const& a, select_args const& b) const {
@@ -103,13 +103,13 @@ namespace sls {
         euf::enode* mk_select(euf::egraph& g, euf::enode* b, euf::enode* sel);
 
         void resolve_conflict();
-        size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
+        size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); }
         size_t* to_ptr(euf::enode* t) { return reinterpret_cast<size_t*>((reinterpret_cast<size_t>(t) << 4) + 1); }
         size_t* to_ptr(unsigned n) { return reinterpret_cast<size_t*>((size_t)(n << 4) + 3); }
         bool is_literal(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 0; }
         bool is_index(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 3; }
         bool is_enode(size_t* p) { return (reinterpret_cast<size_t>(p) & 3) == 1; }
-        sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
+        sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); }
         euf::enode* to_enode(size_t* p) { return reinterpret_cast<euf::enode*>(reinterpret_cast<size_t>(p) >> 4); }
         unsigned to_index(size_t* p) { return static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4); }
         

src/ast/sls/sls_bv_lookahead.cpp

@@ -871,8 +871,8 @@ namespace sls {
         if (m_la.m_config.use_top_level_assertions)
             return m_la.ctx.input_assertions().get(idx);
         return m_la.ctx.atom(m_la.ctx.root_literals()[idx].var());
-    };
+    }
 
 
 
-}
+}

src/ast/sls/sls_bv_tracker.h

@@ -40,7 +40,7 @@ class sls_tracker {
     mpz                   m_zero, m_one, m_two;
 
     struct value_score {
-        value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
+        value_score() : value(unsynch_mpz_manager::mk_z(0)) {}
         value_score(value_score&&) noexcept = default;
         value_score(const value_score &other) {
             m = other.m;

src/ast/sls/sls_context.h

@@ -44,15 +44,15 @@ namespace sls {
         virtual expr_ref get_value(expr* e) = 0;
         virtual bool is_fixed(expr* e, expr_ref& value) { return false; }
         virtual void initialize() = 0;
-        virtual void start_propagation() {};
+        virtual void start_propagation() {}
         virtual bool propagate() = 0;
         virtual void propagate_literal(sat::literal lit) = 0;
         virtual void repair_literal(sat::literal lit) = 0;
         virtual bool repair_down(app* e) = 0;
         virtual void repair_up(app* e) = 0;
         virtual bool is_sat() = 0;
-        virtual void on_rescale() {};
+        virtual void on_rescale() {}
-        virtual void on_restart() {};
+        virtual void on_restart() {}
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual bool set_value(expr* e, expr* v) = 0;
         virtual void collect_statistics(statistics& st) const = 0;

src/ast/sls/sls_euf_plugin.h

@@ -52,8 +52,8 @@ namespace sls {
 
         bool is_user_sort(sort* s) { return s->get_family_id() == user_sort_family_id; }
 
-        size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); };
+        size_t* to_ptr(sat::literal l) { return reinterpret_cast<size_t*>((size_t)(l.index() << 4)); }
-        sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); };
+        sat::literal to_literal(size_t* p) { return sat::to_literal(static_cast<unsigned>(reinterpret_cast<size_t>(p) >> 4)); }
 
         void validate_model();
         void log_clause(sat::literal_vector const& lits);

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -581,7 +581,7 @@ class mbp_qel_cmd : public cmd {
     ptr_vector<expr> m_vars;
 
   public:
-    mbp_qel_cmd() : cmd("mbp-qel"){};
+    mbp_qel_cmd() : cmd("mbp-qel"){}
     char const *get_usage() const override { return "(exprs) (vars)"; }
     char const *get_descr(cmd_context &ctx) const override {
         return "Model based projection using e-graphs";
@@ -639,7 +639,7 @@ class qel_cmd : public cmd {
     ptr_vector<func_decl> m_vars;
 
   public:
-    qel_cmd() : cmd("qel"){};
+    qel_cmd() : cmd("qel"){}
     char const *get_usage() const override { return "(lits) (vars)"; }
     char const *get_descr(cmd_context &ctx) const override {
         return "QE lite over e-graphs";
@@ -703,7 +703,7 @@ class qe_lite_cmd : public cmd {
     ptr_vector<func_decl> m_vars;
 
   public:
-    qe_lite_cmd() : cmd("qe-lite"){};
+    qe_lite_cmd() : cmd("qe-lite"){}
     char const *get_usage() const override { return "(lits) (vars)"; }
     char const *get_descr(cmd_context &ctx) const override {
         return "QE lite over e-graphs";

src/cmd_context/tptp_frontend.cpp

@@ -1011,6 +1011,10 @@ class tptp_parser {
         // Table-driven prefix operator dispatch
         auto op_it = m_ops.find(n);
         if (op_it != m_ops.end() && !op_it->second.is_infix) {
+            if (args.empty()) {
+                while (accept(token_kind::at_tok))
+                    args.push_back(parse_at_arg());
+            }
             return op_it->second.builder(args);
         }
 
@@ -1491,6 +1495,10 @@ class tptp_parser {
         // Table-driven prefix operator dispatch
         auto op_it = m_ops.find(n);
         if (op_it != m_ops.end() && !op_it->second.is_infix) {
+            if (args.empty()) {
+                while (accept(token_kind::at_tok))
+                    args.push_back(parse_at_arg());
+            }
             return op_it->second.builder(args);
         }
 
@@ -1808,8 +1816,19 @@ class tptp_parser {
             expect(token_kind::rparen, "')'");
 
         if (t.domain.empty() && is_ttype(t.range)) {
-            // Sort declaration: monomorphize to m_univ
+            // Sort declaration: give every declared type its own distinct uninterpreted
-            m_sorts.insert_or_assign(name, m_univ);
+            // sort. Collapsing all declared $tType sorts onto a single m_univ is unsound:
+            // a per-type constraint such as "![H:human]:H=jon" would then also constrain
+            // unrelated sorts (e.g. cats), turning satisfiable axiom sets into a spurious
+            // contradiction and reporting Theorem where the conjecture is CounterSatisfiable.
+            if (m_sorts.find(name) == m_sorts.end()) {
+                sort* s = m.mk_uninterpreted_sort(symbol(name));
+                m_pinned_sorts.push_back(s);
+                m_sorts.emplace(name, s);
+            }
+            // A prior *use* of the name (before its declaration) already created a fresh
+            // sort via parse_defined_sort; keep that same sort so uses and the declaration
+            // agree.
             return;
         }
 

src/math/grobner/pdd_simplifier.cpp

@@ -494,7 +494,7 @@ namespace dd {
                 hash(unsigned_vector& vars):vars(vars) {}
                 bool operator()(mon const& m) const {
                     return unsigned_ptr_hash(vars.data() + m.offset, m.sz, 1);
-                };
+                }
             };
             struct eq {
                 unsigned_vector& vars;

src/math/lp/lp_primal_core_solver.h

@@ -267,7 +267,7 @@ namespace lp {
         unsigned j, const T &m, X &theta, bool &unlimited) {
         SASSERT(m > 0 && this->m_column_types[j] == column_type::upper_bound);
         limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
-    };
+    }
 
     void get_bound_on_variable_and_update_leaving_precisely(
         unsigned j, vector<unsigned> &leavings, T m, X &t,

src/math/lp/nla_types.h

@@ -43,9 +43,9 @@ namespace nla {
         ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {}
         bool operator==(const ineq& a) const = delete;
         bool operator!=(const ineq& a) const = delete;
-        const lp::lar_term& term() const { return m_term; };
+        const lp::lar_term& term() const { return m_term; }
-        lp::lconstraint_kind cmp() const { return m_cmp;  };
+        lp::lconstraint_kind cmp() const { return m_cmp;  }
-        const rational& rs() const { return m_rs; };
+        const rational& rs() const { return m_rs; }
     };
     
     class lemma {

src/math/polynomial/algebraic_numbers.cpp

@@ -3511,4 +3511,4 @@ namespace algebraic_numbers {
     void manager::collect_statistics(statistics & st) const {
         m_imp->collect_statistics(st);
     }
-};
+}

src/math/polynomial/algebraic_numbers.h

@@ -410,7 +410,7 @@ namespace algebraic_numbers {
         anum& operator=(basic_cell* cell) { SASSERT(is_null());  m_cell = TAG(void*, cell, BASIC); return *this; }
         anum& operator=(algebraic_cell* cell) { SASSERT(is_null());  m_cell = TAG(void*, cell, ROOT); return *this; }
     };
-};
+}
 
 typedef algebraic_numbers::manager anum_manager;
 typedef algebraic_numbers::manager::numeral anum;

src/math/polynomial/polynomial.cpp

@@ -8253,7 +8253,7 @@ namespace polynomial {
         p->display_smt2(out, m_imp->m_manager, proc);
         return out;
     }
-};
+}
 
 polynomial::polynomial * convert(polynomial::manager & sm, polynomial::polynomial * p, polynomial::manager & tm,
                                  polynomial::var x, unsigned max_d) {

src/math/polynomial/polynomial.h

@@ -36,7 +36,7 @@ class small_object_allocator;
 namespace algebraic_numbers {
     class anum;
     class manager;
-};
+}
 
 namespace polynomial {
     typedef unsigned var;
@@ -1065,7 +1065,7 @@ namespace polynomial {
         scoped_set_zp(manager & _m, uint64_t p):m(_m), m_modular(m.modular()), m_p(m.m()) {  m_p = m.p(); m.set_zp(p); }
         ~scoped_set_zp() {  if (m_modular) m.set_zp(m_p); else m.set_z(); }
     };
-};
+}
 
 typedef polynomial::polynomial_ref           polynomial_ref;
 typedef polynomial::polynomial_ref_vector    polynomial_ref_vector;

src/math/polynomial/polynomial_cache.cpp

@@ -256,4 +256,4 @@ namespace polynomial {
         dealloc(m_imp);
         m_imp = alloc(imp, _m);
     }
-};
+}

src/math/polynomial/polynomial_cache.h

@@ -40,4 +40,4 @@ namespace polynomial {
         void factor(polynomial const * p, polynomial_ref_vector & distinct_factors);
         void reset();
     };
-};
+}

src/math/polynomial/polynomial_primes.h

@@ -66,5 +66,5 @@ namespace polynomial {
     };
 #endif
 
-};
+}
 

src/math/polynomial/polynomial_var2value.h

@@ -43,6 +43,6 @@ namespace polynomial {
         }
     };
     
-};
+}
 
 

src/math/polynomial/rpolynomial.cpp

@@ -789,4 +789,4 @@ namespace rpolynomial {
     }
 #endif
 
-};
+}

src/math/polynomial/rpolynomial.h

@@ -175,7 +175,7 @@ namespace rpolynomial {
             return out;
         }
     };
-};
+}
 
 typedef rpolynomial::polynomial_ref          rpolynomial_ref;
 typedef rpolynomial::polynomial_ref_vector   rpolynomial_ref_vector;

src/math/polynomial/upolynomial.cpp

@@ -3142,4 +3142,4 @@ namespace upolynomial {
         }
         return out;
     }
-};
+}

src/math/polynomial/upolynomial.h

@@ -917,4 +917,4 @@ namespace upolynomial {
         std::ostream& display(std::ostream & out, upolynomial_sequence const & seq, char const * var_name = "x") const;
     };
 
-};
+}

src/math/polynomial/upolynomial_factorization.cpp

@@ -1299,4 +1299,4 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
     return factor_square_free(upm, f, fs, 1, params);
 }
 
-}; // end upolynomial namespace
+} // end upolynomial namespace

src/math/polynomial/upolynomial_factorization.h

@@ -90,5 +90,5 @@ namespace upolynomial {
        That is, the factors of f are inserted as factors of degree k into fs.
     */
     bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, unsigned k, factor_params const & ps = factor_params());
-};
+}
 

src/math/polynomial/upolynomial_factorization_int.h

@@ -416,5 +416,5 @@ namespace upolynomial {
             }
         }
     };
-};
+}
 

src/math/realclosure/realclosure.cpp

@@ -6486,7 +6486,7 @@ namespace realclosure {
     {
         return m_imp->get_sign_condition_coefficient(a, i, j);
     }
-};
+}
 
 void pp(realclosure::manager::imp * imp, realclosure::polynomial const & p, realclosure::extension * ext) {
     imp->display_polynomial_expr(std::cout, p, ext, false, false);

src/math/realclosure/realclosure.h

@@ -317,7 +317,7 @@ namespace realclosure {
         void * data() { return m_value; }
         static num mk(void * ptr) { num r; r.m_value = reinterpret_cast<value*>(ptr); return r; }
     };
-};
+}
 
 typedef realclosure::manager             rcmanager;
 typedef rcmanager::numeral               rcnumeral;

src/math/simplex/simplex.cpp

@@ -74,4 +74,4 @@ namespace simplex {
             }
         }
     }
-};
+}

src/math/simplex/simplex.h

@@ -204,5 +204,5 @@ namespace simplex {
 
     void kernel(sparse_matrix<mpq_ext>& s, vector<vector<rational>>& K);
     void kernel_ffe(sparse_matrix<mpq_ext> &s, vector<vector<rational>> &K);
-};
+}
 

src/math/simplex/simplex_def.h

@@ -1035,6 +1035,6 @@ namespace simplex {
     }
         
 
-};
+}
 
 

src/math/simplex/sparse_matrix.h

@@ -355,4 +355,4 @@ namespace simplex {
         typedef unsynch_mpq_inf_manager eps_manager;
     };
 
-};
+}

src/math/simplex/sparse_matrix_def.h

@@ -603,5 +603,5 @@ namespace simplex {
 
     
 
-};
+}
 

src/math/subpaving/subpaving.cpp

@@ -271,4 +271,4 @@ namespace subpaving {
         return alloc(context_mpfx_wrapper, lim, m, qm, p, a);
     }
 
-};
+}

src/math/subpaving/subpaving.h

@@ -116,6 +116,6 @@ context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manage
 context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = nullptr);
 context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = nullptr);
 
-};
+}
 
 

src/math/subpaving/subpaving_hwf.h

@@ -42,5 +42,5 @@ public:
  context_hwf(reslimit& lim, f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(lim, config_hwf(m), p, a) {}
 };
 
-};
+}
 

src/math/subpaving/subpaving_mpf.h

@@ -43,5 +43,5 @@ public:
  context_mpf(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(lim, config_mpf(m), p, a) {}
 };
 
-};
+}
 

src/math/subpaving/subpaving_mpff.h

@@ -39,5 +39,5 @@ struct config_mpff {
 
 typedef context_t<config_mpff> context_mpff;
 
-};
+}
 

src/math/subpaving/subpaving_mpfx.h

@@ -39,5 +39,5 @@ struct config_mpfx {
 
 typedef context_t<config_mpfx> context_mpfx;
 
-};
+}
 

src/math/subpaving/subpaving_mpq.h

@@ -37,5 +37,5 @@ struct config_mpq {
 
 typedef context_t<config_mpq> context_mpq;
 
-};
+}
 

src/math/subpaving/subpaving_t.h

@@ -845,5 +845,5 @@ public:
     void operator()();
 };
 
-};
+}
 

src/math/subpaving/subpaving_t_def.h

@@ -1952,4 +1952,4 @@ bool context_t<C>::check_invariant() const {
 }
 
 
-};
+}