From 99cc4747c56e6f605502fe158bf6c72128669851 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Dec 2018 17:21:04 -0800 Subject: [PATCH] fixing #1971 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 87bcf4056..13780529a 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -815,7 +815,9 @@ private: mdl = alloc(model, m); for (sat::bool_var v = 0; v < ll_m.size(); ++v) { expr* n = m_sat_mc->var2expr(v); - if (!n || (is_app(n) && to_app(n)->get_num_args() > 0)) continue; + if (!n || !is_app(n) || to_app(n)->get_num_args() > 0) { + continue; + } switch (sat::value_at(v, ll_m)) { case l_true: mdl->register_decl(to_app(n)->get_decl(), m.mk_true());