diff --git a/src/ast/ast.h b/src/ast/ast.h
index 9dd564206..44466e683 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2020,12 +2020,12 @@ public:
 public:
 
     quantifier * mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, 
-                               int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
+                               int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
                                unsigned num_patterns = 0, expr * const * patterns = nullptr,
                                unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr);
 
     quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
-                           int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
+                           int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
                            unsigned num_patterns = 0, expr * const * patterns = nullptr,
                            unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
         return mk_quantifier(forall_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
@@ -2033,7 +2033,7 @@ public:
     }
 
     quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
-                           int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
+                           int weight = 1, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
                            unsigned num_patterns = 0, expr * const * patterns = nullptr,
                            unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
         return mk_quantifier(exists_k, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,