From cdc89b6193ef219e53cf9293528a8b083f95135d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 12:57:08 -0700 Subject: [PATCH] add get-info :rlimit option to cmd-context to facilitate timeout based repros Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 80cd6373e..8ba830287 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -629,6 +629,7 @@ class get_info_cmd : public cmd { symbol m_reason_unknown; symbol m_all_statistics; symbol m_assertion_stack_levels; + symbol m_rlimit; public: get_info_cmd(): cmd("get-info"), @@ -639,7 +640,8 @@ public: m_status(":status"), m_reason_unknown(":reason-unknown"), m_all_statistics(":all-statistics"), - m_assertion_stack_levels(":assertion-stack-levels") { + m_assertion_stack_levels(":assertion-stack-levels"), + m_rlimit(":rlimit") { } char const * get_usage() const override { return ""; } char const * get_descr(cmd_context & ctx) const override { return "get information."; } @@ -671,6 +673,9 @@ public: else if (opt == m_reason_unknown) { ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown().c_str()) << "\")" << std::endl; } + else if (opt == m_rlimit) { + ctx.regular_stream() << "(:rlimit " << ctx.m().limit().count() << ")" << std::endl; + } else if (opt == m_all_statistics) { ctx.display_statistics(); }