projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89081ba) | patch
added support for division by zero for bit-vector division operators
authorLiana Hadarean <lianahady@gmail.com>
Tue, 13 Nov 2012 04:49:34 +0000 (04:49 +0000)
committerLiana Hadarean <lianahady@gmail.com>
Tue, 13 Nov 2012 04:49:34 +0000 (04:49 +0000)
commit2cf12a56cb9c5eb539d50a39b2764a292d6fd13f
tree3578ca6339a97e4b85c83d1a9f2219aea569aca7tree
parent89081ba6a8a62a117cbfef99aa7c8e4bf0bf1b39commit | diff
added support for division by zero for bit-vector division operators
12 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/bitblast_strategies.cpp diff | blob | history
src/theory/bv/bitblaster.cpp diff | blob | history
src/theory/bv/bv_subtheory_eq.cpp diff | blob | history
src/theory/bv/bv_subtheory_eq.h diff | blob | history
src/theory/bv/kinds diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h 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
src/theory/bv/theory_bv_rewriter.h diff | blob | history
test/regress/regress0/unconstrained/Makefile.am diff | blob | history
test/regress/regress0/unconstrained/bvdiv2.smt2 diff | blob | history