summaryrefslogtreecommitdiff
path: root/test/unit/parser/parser_black.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-06-12 09:07:00 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-06-12 11:07:00 -0500
commitc83ce8f341f88bbffcae8fd2bfbed5c33abf4f66 (patch)
tree913aef18511db45418f26de2ee0f3f892584fcfa /test/unit/parser/parser_black.h
parent9925a54ce86e9b0101563c0ace1b973144490528 (diff)
Refactor parser to define fewer tokens for symbols (#2936)
Diffstat (limited to 'test/unit/parser/parser_black.h')
-rw-r--r--test/unit/parser/parser_black.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 33ad3740a..f2f5f24b6 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -138,6 +138,12 @@ class ParserBlack
.withInputLanguage(d_lang)
.build();
+ if (d_lang == LANG_SMTLIB_V2)
+ {
+ // Use QF_LIA to make multiplication ("*") available
+ static_cast<Smt2*>(parser)->setLogic("QF_LIA");
+ }
+
TS_ASSERT(!parser->done());
setupContext(*parser);
TS_ASSERT(!parser->done());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback