projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 25be5c6) | patch
Ensure mkConstInt is used on integral rationals only (#8683)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Apr 2022 17:49:05 +0000 (12:49 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Apr 2022 17:49:05 +0000 (17:49 +0000)
commit4aa5c467d199e958bd3b0d10ea11fa587e199ae1
tree20a5490fa56e60f8a5a9b41e1f14542c75ae1127tree
parent25be5c6148c0e0d9ab4666062c0666fb085eee8acommit | diff
Ensure mkConstInt is used on integral rationals only (#8683)

This is work towards using CONST_INTEGER for integer constants.

This corrects a few places that incorrectly assumed that integers were necessary.
src/expr/node_manager_template.cpp diff | blob | history
src/proof/proof_rule.cpp diff | blob | history
src/theory/arith/arith_msum.cpp diff | blob | history
src/theory/arith/linear/constraint.cpp diff | blob | history
src/theory/arith/linear/theory_arith_private.cpp diff | blob | history