From db646dda8972168bec8975156f8cffc11a3eda47 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jan 2017 13:33:47 -0800 Subject: [PATCH] fix(library/tactic/smt/smt_state): forgot to set zeta option --- src/library/tactic/smt/smt_state.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index c9377ca1f9..2a30782e7b 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -282,6 +282,7 @@ static expr intros(environment const & env, options const & opts, metavar_contex The nested instances of has_add and has_zero must be canonized and registered at dcs. */ dsimplify_fn dsimp = mk_dsimp(ctx, dcs, s_goal.get_pre_config()); + type_context::zeta_scope _1(ctx, s_goal.get_pre_config().m_zeta); expr target = decl->get_type(); type_context::tmp_locals locals(ctx); buffer new_Hs;