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

include QF_SNIA

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-13 08:13:39 -08:00
parent 943d881340
commit f3e7c8c9df
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/solver/smt_logics.cpp
View file

@ -65,6 +65,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
s == "QF_UFNIA" ||
s == "QF_UFNIRA" ||
s == "QF_BVRE" ||
s == "QF_SNIA" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
@ -136,11 +137,11 @@ bool smt_logics::logic_has_array(symbol const & s) {
}
bool smt_logics::logic_has_seq(symbol const & s) {
return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
return s == "QF_BVRE" || logic_has_str(s);
}
bool smt_logics::logic_has_str(symbol const & s) {
return s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
return s == "QF_S" || s == "QF_SLIA" || s == "QF_SNIA" || logic_is_all(s);
}
bool smt_logics::logic_has_fpa(symbol const & s) {