From a1eee6275f51d00f5d25de2f852f3a2e16e6c243 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 19 Oct 2015 19:03:36 +0100 Subject: [PATCH] Bugfix for C++ examples. Relates to #26 --- examples/c++/example.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 3ef00275e..af972a36b 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1017,6 +1017,7 @@ void extract_example() { x = c.constant("x", c.bv_sort(32)); expr y = x.extract(21, 10); std::cout << y << " " << y.hi() << " " << y.lo() << "\n"; +} void sudoku_example() { std::cout << "sudoku example\n"; @@ -1059,7 +1060,7 @@ void sudoku_example() { // each 3x3 square contains a digit at most once for (unsigned i0 = 0; i0 < 3; i0++) { - for (uint j0 = 0; j0 < 3; j0++) { + for (unsigned j0 = 0; j0 < 3; j0++) { expr_vector t(c); for (unsigned i = 0; i < 3; i++) for (unsigned j = 0; j < 3; j++)