Pull out the solver.

Z3Prover · Apr 5, 2015 · 0f467eb · 0f467eb
1 parent e8b8393
commit 0f467eb
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
@@ -989,8 +989,9 @@ void sudoku_example() {
             x.push_back(c.int_const(x_name.str().c_str()));
         }
 
-    // each cell contains a value in {1, ..., 9}
     solver s(c);
+
+    // each cell contains a value in {1, ..., 9}
     for (unsigned i = 0; i < 9; ++i)
         for (unsigned j = 0; j < 9; ++j) {
             s.add(x[i * 9 + j] >= 1 && x[i * 9 + j] <= 9);