Generalize finite bound inference to unifiable variables in set membership literals.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 7 Feb 2017 19:26:57 +0000 (13:26 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 7 Feb 2017 19:26:57 +0000 (13:26 -0600)
commit3837f84ab251d1563726f3d13b95f541eaa331a4
tree7afb6eb470b837b7e7600437356a8080fc329eb5
parent0dd2aa21f35b221ea96d277e9ea7cbc816ffe83c
Generalize finite bound inference to unifiable variables in set membership literals.
src/options/sets_options
src/theory/quantifiers/bounded_integers.cpp
src/theory/quantifiers/bounded_integers.h
src/theory/sets/theory_sets_private.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/fmf/cons-sets-bounds.smt2 [new file with mode: 0644]