diff options
Diffstat (limited to 'test/unit/expr/node_white.h')
| -rw-r--r-- | test/unit/expr/node_white.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index ce67004c6..a042b1752 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -73,7 +73,7 @@ public: Node x = d_nm->mkVar("x", d_nm->integerType()); Node y = d_nm->mkVar("y", d_nm->integerType()); Node x_plus_y = d_nm->mkNode(PLUS, x, y); - Node two = d_nm->mkConst(Integer(2)); + Node two = d_nm->mkConst(Rational(2)); Node x_times_2 = d_nm->mkNode(MULT, x, two); Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y); |