projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc0e4a6) | patch
Add more general SignExtendUltConst rewriting. (#1385)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 5 Apr 2018 18:40:34 +0000 (11:40 -0700)
committerGitHub <noreply@github.com>
Thu, 5 Apr 2018 18:40:34 +0000 (11:40 -0700)
commitcf73e3ceb3f93fef830349bd44afec99404b5038
tree407c2a4e90e6200244a7301e7f736ff2493813bbtree
parentdc0e4a68281032194a7626050b8fbb74d3f5e183commit | diff
Add more general SignExtendUltConst rewriting. (#1385)

This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history