mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix for mising handling of quantifiers in tactic. Bug #324
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
86f1753ebf
commit
d6d301c5eb
|
@ -305,14 +305,16 @@ public:
|
|||
m_nonfd.mark(f, true);
|
||||
expr* e1, *e2;
|
||||
if (m.is_eq(f, e1, e2)) {
|
||||
if (is_fd(e1, e2)) {
|
||||
if (is_fd(e1, e2) || is_fd(e2, e1)) {
|
||||
continue;
|
||||
}
|
||||
if (is_fd(e2, e1)) {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
|
||||
if (is_app(f)) {
|
||||
m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
|
||||
}
|
||||
else if (is_quantifier(f)) {
|
||||
m_todo.push_back(to_quantifier(f)->get_expr());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue