mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-02 21:37:02 +00:00
Code Activity

fix #4594

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-27 09:22:53 -07:00
parent ae502bc2c4
commit a08082e392
5 changed files with 31 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/parsers/smt2/smt2scanner.cpp
View file

@ -271,6 +271,7 @@ namespace smt2 {
}
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) :
ctx(ctx),
m_interactive(interactive),
m_spos(0),
m_curr(0), // avoid Valgrind warning
@ -283,7 +284,6 @@ namespace smt2 {
m_stream(stream),
m_cache_input(false) {
m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
for (int i = 0; i < 256; ++i) {
m_normalized[i] = (signed char) i;
@ -366,7 +366,7 @@ namespace smt2 {
if (t == NULL_TOKEN) break;
return t;
case '-':
if (m_smtlib2_compliant)
if (ctx.params().m_smtlib2_compliant)
return read_symbol();
else
return read_signed_number();

2
src/parsers/smt2/smt2scanner.h
View file

@ -30,6 +30,7 @@ namespace smt2 {
class scanner {
private:
cmd_context& ctx;
bool m_interactive;
int m_spos; // position in the current line of the stream
char m_curr; // current char;
@ -54,7 +55,6 @@ namespace smt2 {
svector<char> m_cache;
svector<char> m_cache_result;
bool m_smtlib2_compliant;
char curr() const { return m_curr; }
void new_line() { m_line++; m_spos = 0; }