projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 207a450) | patch
A better mechanism for handling BV terms with aliases: inject the alias at the decl_b...
authorGuy <katz911@gmail.com>
Fri, 3 Jun 2016 21:10:42 +0000 (14:10 -0700)
committerGuy <katz911@gmail.com>
Fri, 3 Jun 2016 21:10:42 +0000 (14:10 -0700)
commit90b909a89c78c75afae69e119feea20b478c0795
tree7dae83a6f32375acd4f6220d04579d96c6ef2f19tree
parent207a450e9a48d6cbae663d60b35594085d1a2c01commit | diff
A better mechanism for handling BV terms with aliases: inject the alias at the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
proofs/signatures/th_bv_bitblast.plf diff | blob | history
src/proof/bitvector_proof.cpp diff | blob | history