From 7eee7914bd50885159f52d941f4a9296db69b980 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Oct 2022 15:26:00 -0700 Subject: [PATCH] align format of quantifier instantiation with new core So far the format is (forall ((x Int)) body) (not (body[t/x])) The alternative could be the clause (not (forall ((x Int)) body)) body[t/x] they just better be consistent between engines --- src/smt/qi_queue.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index b3e8429b4..cb28f87f8 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -311,8 +311,8 @@ namespace smt { expr* gens[1] = { gen.get() }; for (unsigned i = 0; i < num_bindings; ++i) bindings_e.push_back(bindings[i]->get_expr()); - args.push_back(m.mk_not(q)); - args.push_back(instance); + args.push_back(q); + args.push_back(mk_not(m, instance)); args.push_back(m.mk_app(symbol("bind"), num_bindings, bindings_e.data(), m.mk_proof_sort())); args.push_back(m.mk_app(symbol("gen"), 1, gens, m.mk_proof_sort())); pr1 = m.mk_app(symbol("inst"), args.size(), args.data(), m.mk_proof_sort());