projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4adff16) | patch
Make iand lemmas use proper Inference types. (#4956)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 28 Aug 2020 00:38:36 +0000 (02:38 +0200)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 00:38:36 +0000 (17:38 -0700)
commit3e057f9d0454738429ade62dbad8f5ac0b3274db
treef028abd6c8775a15dfadbadbc52be0d144daf1catree
parent4adff162770a841d136ec44146928c2296eaf1b2commit | diff
Make iand lemmas use proper Inference types. (#4956)

For some reason, the nl subsolver for IAND did not annotate its lemmas with `Inference` types yet. This commit adds appropriate `Inference` values and makes the IAND solver use them.
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/inference.cpp diff | blob | history
src/theory/arith/nl/inference.h diff | blob | history