diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-05 16:07:07 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-05 16:07:07 -0800 |
commit | 14ec91ed77b816d77de60fbf6e77066da194d791 (patch) | |
tree | 4198f7cee37f0b14d991311ddfbf6367e5309811 /src/smt/smt_engine.cpp | |
parent | 44c278ce99b7d84b070d260196c44569209f1528 (diff) |
Added "dump=raw-benchmark" option for dumping all user commands exactly as received.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f5b769984..30da29813 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1099,11 +1099,14 @@ void SmtEngine::finishInit() { // dump out a set-logic command if(Dump.isOn("benchmark")) { - // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); - LogicInfo everything; - everything.lock(); - Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.") - << SetBenchmarkLogicCommand(everything.getLogicString()); + if (Dump.isOn("raw-benchmark")) { + Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic.getLogicString()); + } else { + LogicInfo everything; + everything.lock(); + Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.") + << SetBenchmarkLogicCommand(everything.getLogicString()); + } } Trace("smt-debug") << "Dump declaration commands..." << std::endl; @@ -4497,6 +4500,10 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; + if (Dump.isOn("raw-benchmark")) { + Dump("raw-benchmark") << AssertCommand(ex); + } + // Substitute out any abstract values in ex Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); |