diff options
Diffstat (limited to 'examples/simple_vc_cxx.cpp')
| -rw-r--r-- | examples/simple_vc_cxx.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 49a4f576e..e648b9994 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -32,16 +32,16 @@ int main() { Term x = slv.mkConst(integer, "x"); Term y = slv.mkConst(integer, "y"); - Term zero = slv.mkReal(0); + Term zero = slv.mkInteger(0); Term x_positive = slv.mkTerm(Kind::GT, x, zero); Term y_positive = slv.mkTerm(Kind::GT, y, zero); - Term two = slv.mkReal(2); + Term two = slv.mkInteger(2); Term twox = slv.mkTerm(Kind::MULT, two, x); Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y); - Term three = slv.mkReal(3); + Term three = slv.mkInteger(3); Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three); Term formula = |