summaryrefslogtreecommitdiff
path: root/examples/api/bitvectors.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-11-27 11:12:11 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-11-27 11:12:26 -0500
commit86b54ede8a2898a6c51fddd4bb32f8b4b87b5da6 (patch)
tree989d5595bb52ba2e9cff08e9dd27ccf65e3b0997 /examples/api/bitvectors.cpp
parentdd7e0c66cab285c154f59ff27132059c34e09e23 (diff)
Incremental is now on by default when using from API, off for command-line driver except in interactive mode.
Diffstat (limited to 'examples/api/bitvectors.cpp')
-rw-r--r--examples/api/bitvectors.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index fa3099336..b69ee5d17 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -25,8 +25,7 @@ using namespace CVC4;
int main() {
ExprManager em;
SmtEngine smt(&em);
- smt.setOption("incremental", true); // Enable incremental solving
- smt.setLogic("QF_BV"); // Set the logic
+ smt.setLogic("QF_BV"); // Set the logic
// The following example has been adapted from the book A Hacker's Delight by
// Henry S. Warren.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback