From 4dbccbf23a0afe81af19358a70faf88926b02936 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Apr 2019 14:11:40 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/smt/theory_special_relations.cpp | 8 ++++---- src/smt/theory_special_relations.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 03f11dd26..07fd42ad6 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -336,7 +336,7 @@ namespace smt { continue; } expr_ref f_app(m.mk_app(f, arg1, arg2), m); - enode* fn = ensure_enode(f_app); + ensure_enode(f_app); literal f_lit = ctx.get_literal(f_app); switch (ctx.get_assignment(f_lit)) { case l_true: @@ -984,7 +984,7 @@ Take 2: expr* A = AV, *dst = dstV, *S = SV; expr_ref connected_body(m); - connected_body = m.mk_app(pair, nilc, S); + connected_body = m.mk_app(pair, nilc.get(), S); for (atom* ap : r.m_asserted_atoms) { atom& a = *ap; @@ -996,8 +996,8 @@ Take 2: expr* args[5] = { x, y, A, S, cb }; connected_body = m.mk_app(nextf, 5, args); } - expr_ref Ap(m.mk_app(fst, connected_body), m); - expr_ref Sp(m.mk_app(snd, connected_body), m); + expr_ref Ap(m.mk_app(fst, connected_body.get()), m); + expr_ref Sp(m.mk_app(snd, connected_body.get()), m); connected_body = m.mk_ite(m.mk_eq(Ap, nilc), F, m.mk_ite(m.mk_app(memf, dst, Ap), T, diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index fd88cc456..83beb35bb 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -175,7 +175,7 @@ namespace smt { literal mk_literal(expr* _e); enode* ensure_enode(expr* e); - theory_var mk_var(enode* n); + theory_var mk_var(enode* n) override; void collect_asserted_po_atoms(vector< std::pair >& atoms) const; void display_atom(std::ostream & out, atom& a) const;