mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #7590 logic alphabet soup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-19 08:57:23 -10:00
parent 03f18c148e
commit 30021dd74f
1 changed files with 2 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/solver/smt_logics.cpp
View file

@ -70,14 +70,8 @@ bool smt_logics::logic_has_bv(symbol const & s) {
bool smt_logics::logic_has_array(symbol const & s) {
return
s.str().find("QF_A") != std::string::npos ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
s == "AUFNIRA" ||
s == "AUFBV" ||
s == "ABV" ||
s.str().starts_with("QF_A") ||
s.str().starts_with("A") ||
logic_is_all(s) ||
s == "SMTFD" ||
s == "HORN";