summaryrefslogtreecommitdiff
path: root/src/smt/smt_solver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_solver.cpp')
-rw-r--r--src/smt/smt_solver.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d7b70f501..f5783ab6b 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as)
// Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
- TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
const std::vector<Node>& assertions = ap.ref();
// It is important to distinguish the input assertions from the skolem
// definitions, as the decision justification heuristic treates the latter
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback