Fix dumping of get-unsat-assumptions (#2302)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 15 Aug 2018 16:37:00 +0000 (09:37 -0700)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 15 Aug 2018 16:37:00 +0000 (09:37 -0700)
commite09be1045fc6cc8c5373f9eb96137add66b8d5d5
treeb7e7b133524287aba7fda1cdda195df039f46e70
parent4a3bde6335f676a28f4aa5f872c213e0ec8bbaa7
Fix dumping of get-unsat-assumptions (#2302)

When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.
src/smt/smt_engine.cpp
src/smt/smt_engine.h