fix #2664

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/parsers/smt2/smt2parser.cpp

@@ -411,6 +411,7 @@ namespace smt2 {
 
         bool curr_id_is_underscore() const { SASSERT(curr_is_identifier()); return curr_id() == m_underscore; }
         bool curr_id_is_as() const { SASSERT(curr_is_identifier()); return curr_id() == m_as; }
+        bool curr_id_is_reserved() const { return curr_id_is_underscore() || curr_id_is_as(); }
         bool curr_id_is_match() const { SASSERT(curr_is_identifier()); return curr_id() == m_match; }
         bool curr_id_is_case() const { return curr_id() == m_case; }
         bool curr_id_is_forall() const { SASSERT(curr_is_identifier()); return curr_id() == m_forall; }
@@ -427,10 +428,11 @@ namespace smt2 {
             if (!curr_is_identifier() || curr_id() != id)
                 throw parser_exception(msg);
             next();
-        }
+        }        
         void check_underscore_next(char const * msg) { check_id_next(m_underscore, msg); }
         void check_as_next(char const * msg) { check_id_next(m_as, msg); }
         void check_identifier(char const * msg) { if (!curr_is_identifier()) throw parser_exception(msg); }
+        void check_nonreserved_identifier(char const * msg) { if (!curr_is_identifier() || curr_id_is_reserved()) throw parser_exception(msg); }
         void check_keyword(char const * msg) { if (!curr_is_keyword()) throw parser_exception(msg); }
         void check_string(char const * msg) { if (!curr_is_string()) throw parser_exception(msg); }
         void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
@@ -2163,7 +2165,7 @@ namespace smt2 {
             check_lparen_next("invalid sort declaration, parameters missing");
             unsigned i = 0;
             while (!curr_is_rparen()) {
-                check_identifier("invalid sort parameter, symbol or ')' expected");
+                check_nonreserved_identifier("invalid sort parameter, symbol or ')' expected");
                 m_sort_id2param_idx.insert(curr_id(), i);
                 i++;
                 next();
@@ -2214,7 +2216,7 @@ namespace smt2 {
             SASSERT(curr_id() == m_declare_sort);
             next();
 
-            check_identifier("invalid sort declaration, symbol expected");
+            check_nonreserved_identifier("invalid sort declaration, symbol expected");
             symbol id = curr_id();
             if (m_ctx.find_psort_decl(id) != nullptr)
                 throw parser_exception("invalid sort declaration, sort already declared/defined");
@@ -2239,7 +2241,7 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_define_sort);
             next();
-            check_identifier("invalid sort definition, symbol expected");
+            check_nonreserved_identifier("invalid sort definition, symbol expected");
             symbol id = curr_id();
             if (m_ctx.find_psort_decl(id) != nullptr)
                 throw parser_exception("invalid sort definition, sort already declared/defined");
@@ -2260,7 +2262,7 @@ namespace smt2 {
             SASSERT(curr_id() == (is_fun ? m_define_fun : m_model_add));
             SASSERT(m_num_bindings == 0);
             next();
-            check_identifier("invalid function/constant definition, symbol expected");
+            check_nonreserved_identifier("invalid function/constant definition, symbol expected");
             symbol id = curr_id();
             next();
             unsigned sym_spos  = symbol_stack().size();
@@ -2460,7 +2462,7 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_declare_fun);
             next();
-            check_identifier("invalid function declaration, symbol expected");
+            check_nonreserved_identifier("invalid function declaration, symbol expected");
             symbol id = curr_id();
             next();
             unsigned spos = sort_stack().size();
@@ -2479,7 +2481,7 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_declare_const);
             next();
-            check_identifier("invalid constant declaration, symbol expected");
+            check_nonreserved_identifier("invalid constant declaration, symbol expected");
             symbol id = curr_id();
             next();
             parse_sort("Invalid constant declaration");

src/util/mpz.cpp

@@ -46,6 +46,7 @@ Revision History:
 #define LEHMER_GCD
 #endif
 
+
 #if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
 // This is needed for _tzcnt_u32 and friends.
 #include <immintrin.h>