From 823bf317c5d420c971cecaab94dc43fdc20f0f49 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Oct 2019 05:11:24 -0700
Subject: [PATCH] fix #2664
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/parsers/smt2/smt2parser.cpp | 16 +++++++++-------
src/util/mpz.cpp | 1 +
2 files changed, 10 insertions(+), 7 deletions(-)
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 3e2faf7be..d9084f11b 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/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");
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 433867626..a8190df1b 100644
--- a/src/util/mpz.cpp
+++ b/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>