projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a37f486) | patch
Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Sep 2021 15:31:07 +0000 (10:31 -0500)
committerGitHub <noreply@github.com>
Tue, 14 Sep 2021 15:31:07 +0000 (15:31 +0000)
commitefdefd95abd7de85963b9dd22e98e2858864cb07
tree1108123b3f08ac66d6db5a002955891e9a398809tree
parenta37f486c6e10b882a81474418e1d3f4ffdbd583ccommit | diff
Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)

Printing the original benchmark is simple, as it is exactly the commands we execute.

This removes the previous code from SmtEngine, which is currently broken.
src/main/command_executor.cpp diff | blob | history
src/options/base_options.toml diff | blob | history
src/smt/command.h diff | blob | history
src/smt/dump.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
test/regress/regress0/datatypes/datatype-dump.cvc diff | blob | history
test/regress/regress0/printer/let_shadowing.smt2 diff | blob | history
test/regress/run_regression.py diff | blob | history
test/unit/api/solver_black.cpp diff | blob | history