diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-13 16:42:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-13 22:42:38 +0000 |
| commit | f66ed2f3f12b82c99f0dc8620acdd313b62b840e (patch) | |
| tree | 4688eef5b8326468f8e5f0172a63a3623915ca0e /src/theory/bags | |
| parent | 9b81d04da42615642c2fd4ec6b4637862848ae0a (diff) | |
Distinguishing more uses of CONST_RATIONAL (#7802)
Towards eliminating subtyping Int/Real.
Diffstat (limited to 'src/theory/bags')
| -rw-r--r-- | src/theory/bags/bag_reduction.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bags/bag_reduction.cpp b/src/theory/bags/bag_reduction.cpp index 6e1b4c1a5..3e6544882 100644 --- a/src/theory/bags/bag_reduction.cpp +++ b/src/theory/bags/bag_reduction.cpp @@ -65,8 +65,8 @@ Node BagReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts) Node f = node[0]; Node t = node[1]; Node A = node[2]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(Rational(1)); // types TypeNode bagType = A.getType(); TypeNode elementType = A.getType().getBagElementType(); |