From de3ead9ff14c5761cccf4ffd7e6e0afe48ab521f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 28 Sep 2015 18:20:22 +0100 Subject: [PATCH] build fix --- src/tactic/fpa/fpa2bv_model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index f0b745764..f0a25a9d5 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -215,7 +215,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { #else SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT); SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT); - seen.insert(to_app(to_app(a->get_arg(0))->get_arg(0))->get_decl()); + seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl()); #endif if (!sgn && !sig && !exp)