projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 103d6a6) | patch
Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE...
authorClark Barrett <barrett@cs.nyu.edu>
Sun, 10 Jun 2012 14:43:58 +0000 (14:43 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Sun, 10 Jun 2012 14:43:58 +0000 (14:43 +0000)
commit48f837c9d53e2e93b14786943f9961228e0d9933
tree6caf8bc4dc9e6d937b7db30587257504be632589tree
parent103d6a6aad30410f8d7546c25c1f5e67f1c334d7commit | diff
Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE_DONE" is idempotent
Found several problems where this is not the case and fixed them
src/theory/bv/theory_bv_rewrite_rules_normalization.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
src/theory/rewriter.cpp diff | blob | history