diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-04 14:55:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-04 19:55:13 +0000 |
| commit | e680a299ac1da58b8fee27e3733d5e5eea255d94 (patch) | |
| tree | f04aa45a3dd49064010bf0c883f1b9a508cda996 /src/smt/check_models.cpp | |
| parent | 67559f3b3e42dc1937f809e56ee57daa4bd8bd89 (diff) | |
Replace the old dump infrastructure (#7572)
This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks.
This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain.
This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync.
The other dumping tags are deleted for now, and will be reimplemented as needed.
Diffstat (limited to 'src/smt/check_models.cpp')
| -rw-r--r-- | src/smt/check_models.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 13e504835..d7f654fc6 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -18,7 +18,6 @@ #include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/node_command.h" #include "smt/preprocessor.h" #include "smt/smt_solver.h" #include "theory/rewriter.h" |