mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
srp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a95c35dadb
commit
a52303c4fb
|
@ -73,7 +73,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
|
|||
}
|
||||
if (m_args.size() == n) {
|
||||
if (arg_differs) {
|
||||
b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
|
||||
b = m.mk_app(c->get_decl(), m_args);
|
||||
m_refs.push_back(b);
|
||||
SASSERT(m.get_sort(a) == m.get_sort(b));
|
||||
} else {
|
||||
|
|
Loading…
Reference in a new issue