diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 07b555095..dc051bd71 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -192,7 +192,8 @@ def_module_params('fixedpoint', ('spacer.quic_gen_normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.share_lemmas', BOOL, False, "Share frame lemmas"), ('spacer.share_invariants', BOOL, False, "Share invariants lemmas"), -)) + ('spacer.from_level', UINT, 0, 'starting level to explore') + )) diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp index 57c225b38..69e5d76ff 100644 --- a/src/muz/spacer/spacer_dl_interface.cpp +++ b/src/muz/spacer/spacer_dl_interface.cpp @@ -170,7 +170,7 @@ lbool dl_interface::query(expr * query) return l_false; } - return m_context->solve(); + return m_context->solve(m_ctx.get_params().spacer_from_level()); }