projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce6d8fd) | patch
Fix handling for UGT/SGT. (#1467)
authorMathias Preiner <mathias.preiner@gmail.com>
Wed, 3 Jan 2018 00:54:32 +0000 (16:54 -0800)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 3 Jan 2018 00:54:32 +0000 (16:54 -0800)
commitf8f8103229a9b84e944148985ebb05abed814619
tree0e3ed240518f99c819feceaade6fd9273068baaetree
parentce6d8fde786eb6b4bb658ba83afd384d02853948commit | diff
Fix handling for UGT/SGT. (#1467)

Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk
if we encounter a literal t < x s.
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history