mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Added new SMT logic names

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-06 16:24:44 +00:00
parent ebbed7a92e
commit c2aee86e4e
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/cmd_context.cpp
View file

@ -507,6 +507,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "QF_ANIA" ||
s == "QF_LIRA" ||
s == "QF_UFLIA" ||
s == "QF_UFLRA" ||
s == "QF_UFIDL" ||
@ -518,6 +520,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_UFNIA" ||
s == "QF_UFNIRA" ||
s == "QF_BVRE" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
@ -526,9 +529,12 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "UFLRA" ||
s == "UFNRA" ||
s == "UFNIRA" ||
s == "NIA" ||
s == "NRA" ||
s == "UFNIA" ||
s == "LIA" ||
s == "LRA" ||
s == "UFIDL" ||
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
@ -583,10 +589,12 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
return
s == "QF_AX" ||
s == "QF_AUFLIA" ||
s == "QF_ANIA" ||
s == "QF_ALIA" ||
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||