From b8c373bbce423f861cb1583dbc73d53fa987e3d6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 22 Dec 2014 14:25:23 +0000 Subject: [PATCH] fpa2bv tactic bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 4a3a01b6f..5fb35d972 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -96,8 +96,8 @@ class fpa2bv_tactic : public tactic { g->inc_depth(); result.push_back(g.get()); - for (unsigned i = 0; i < m_conv.extra_assertions.size(); i++) - result.back()->assert_expr(m_conv.extra_assertions[i].get()); + for (unsigned i = 0; i < m_conv.m_extra_assertions.size(); i++) + result.back()->assert_expr(m_conv.m_extra_assertions[i].get()); SASSERT(g->is_well_sorted()); TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout);