diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:04:35 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:28:24 -0400 |
| commit | 16215e6e021c0fb24a6237126e17c89485dfc012 (patch) | |
| tree | 484f927a27af4d26c616d5982e0b0ce2497eaad7 /test | |
| parent | 118e998b926870e817cd57c49b91fdb27948e828 (diff) | |
Some model and printing fixes for defined functions in input.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/expr/type_node_white.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 86f0b192d..97dc1a696 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -61,7 +61,7 @@ public: TypeNode bvType = d_nm->mkBitVectorType(32); TypeNode subrangeType = d_nm->mkSubrangeType(SubrangeBounds(Integer(1), Integer(10))); - Node x = d_nm->mkVar("x", realType); + Node x = d_nm->mkBoundVar("x", realType); Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0))); TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType); Node lambda = d_nm->mkVar("lambda", funtype); |