mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

fix #1484

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-12 23:30:10 -08:00
parent 792fdb915f
commit eab7ae58be
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.cpp
View file

@ -320,7 +320,7 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
if (d.m_domain.size() != n) continue; if (d.m_domain.size() != n) continue;
bool eq = true; bool eq = true;
for (unsigned i = 0; eq && i < n; ++i) { for (unsigned i = 0; eq && i < n; ++i) {
eq = d.m_domain[i] == m().get_sort(args[i]); eq = m().compatible_sorts(d.m_domain[i], m().get_sort(args[i]));
} }
if (eq) { if (eq) {
t = d.m_body; t = d.m_body;