projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 278b609) | patch
Simplify atoms introduced while bitblasting. (#1267)
authorMathias Preiner <mathias.preiner@gmail.com>
Sat, 21 Oct 2017 02:01:51 +0000 (19:01 -0700)
committerGitHub <noreply@github.com>
Sat, 21 Oct 2017 02:01:51 +0000 (19:01 -0700)
commit7908fd9c901c056628f5f3846049d078d48bc396
tree91e90498c5f0e9e0c4ab9005eaf0531ad41a128ctree
parent278b60971f6209ffc0eb76a23548c081dc8c9c56commit | diff
Simplify atoms introduced while bitblasting. (#1267)

If a newly introduced atom is not rewritten it can happen that the
literals of both the original atom and the rewritten atom end up in the CNF.
However, only the original atom has a BB definition and the literal of the
rewritten atom is unconstrained (no BB definition).
src/theory/bv/bitblast_strategies_template.h diff | blob | history