projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eaad5bd) | patch
Add proofs to TheoryArithPrivate::propagate (#5812)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 26 Jan 2021 04:20:58 +0000 (20:20 -0800)
committerGitHub <noreply@github.com>
Tue, 26 Jan 2021 04:20:58 +0000 (22:20 -0600)
commit909a0aa67266d7659decf56f2e6eb8101a802d45
treeb435672d7efe2649ce36f43d2c3844ed44cf0304tree
parenteaad5bdc7a38fcc38baa0e3b73f6c39a0ec6fb05commit | diff
Add proofs to TheoryArithPrivate::propagate (#5812)

Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.
src/theory/arith/theory_arith_private.cpp diff | blob | history