summaryrefslogtreecommitdiff
path: root/proofs/signatures/sat.plf
diff options
context:
space:
mode:
authorGuy <katz911@gmail.com>2016-06-03 14:10:42 -0700
committerGuy <katz911@gmail.com>2016-06-03 14:10:42 -0700
commit90b909a89c78c75afae69e119feea20b478c0795 (patch)
tree7dae83a6f32375acd4f6220d04579d96c6ef2f19 /proofs/signatures/sat.plf
parent207a450e9a48d6cbae663d60b35594085d1a2c01 (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
Diffstat (limited to 'proofs/signatures/sat.plf')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback