diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-21 12:14:18 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-21 12:14:18 -0700 |
| commit | a72771b2f04eb5f761c9db59435165d7cdcdf688 (patch) | |
| tree | cbc1f017578712a147a52d27c12488a03ba231b7 /src/smt/smt_solver.cpp | |
| parent | bf3af55b4509ec2abf8806187d8c1765e2d8330c (diff) | |
| parent | 331187d557b2c54b079de6348ff1f597a72f50a2 (diff) | |
Merge branch 'master' into rmCDAttrrmCDAttr
Diffstat (limited to 'src/smt/smt_solver.cpp')
| -rw-r--r-- | src/smt/smt_solver.cpp | 1 |
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 |