projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 16578fc) | patch
Eliminating spurious replay of commands for define funs expansion when checking unsat...
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 25 Aug 2020 18:00:11 +0000 (15:00 -0300)
committerGitHub <noreply@github.com>
Tue, 25 Aug 2020 18:00:11 +0000 (15:00 -0300)
commitc5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2
tree24ca2e0802a18c5ec27d50dd793a2b3a6ccf5a41tree
parent16578fca1c50d2ca9fce45c9c262db7ff6e2fd92commit | diff
Eliminating spurious replay of commands for define funs expansion when checking unsat cores (#4941)

Doing it via commands being added to the coreChecker SMT engine is not necessary since we can directly add assertions after expansion from the original SMT engine.
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history