projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4106b93) | patch
Always ensure literal when requiring phase via inference manager (#8292)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 12 Mar 2022 00:26:37 +0000 (18:26 -0600)
committerGitHub <noreply@github.com>
Sat, 12 Mar 2022 00:26:37 +0000 (00:26 +0000)
commit27b472240649f4fc6a9a2819282711300b426ba6
treedae319cfe2876f0de132aa06305f17d57a824904tree
parent4106b9314285c4f8641af414566e9382e2e1bfeccommit | diff
Always ensure literal when requiring phase via inference manager (#8292)

Also to be safe, ensures we clear pending in quantifiers engine.

Fixes cvc5/cvc5-projects#484.
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history
test/api/cpp/CMakeLists.txt diff | blob | history
test/api/cpp/proj-issue484.cpp [new file with mode: 0644] blob