Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

8 files changed, 4 insertions, 12 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.
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index f20f5f13c..4533e35e1 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -45,7 +45,6 @@ int main() {
   ExprManager em;
   SmtEngine smt(&em);
   smt.setOption("produce-models", true); // Produce Models
-  smt.setOption("incremental", true); // Enable Multiple Queries
   smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's
   smt.setOption("default-dag-thresh", 0); //Disable dagifying the output
   smt.setLogic(string("QF_UFLIRA"));
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index eb3e1642e..f6e719735 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -23,8 +23,7 @@ public class BitVectors {
     ExprManager em = new ExprManager();
     SmtEngine smt = new SmtEngine(em);
 
-    smt.setOption("incremental", new SExpr(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.
diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java
index 0b0984bf3..b619b053e 100644
--- a/examples/api/java/CVC4Streams.java
+++ b/examples/api/java/CVC4Streams.java
@@ -22,7 +22,6 @@ public class CVC4Streams {
     System.loadLibrary("cvc4jni");
     ExprManager exprMgr = new ExprManager();
     SmtEngine smt = new SmtEngine(exprMgr);
-    smt.setOption("incremental", new SExpr(true));
     smt.setOption("output-language", new SExpr("smt2"));
 
     PipedOutputStream solverPipe = new PipedOutputStream();
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 283e24a5f..b529f6316 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -41,7 +41,6 @@ public class Combination {
 
     smt.setOption("tlimit", new SExpr(100));
     smt.setOption("produce-models", new SExpr(true)); // Produce Models
-    smt.setOption("incremental", new SExpr(true)); // Enable Multiple Queries
     smt.setOption("output-language", new SExpr("cvc4")); // output-language
     smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output
     smt.setLogic("QF_UFLIRA");
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index f03dc7f85..582c2ab21 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -24,8 +24,7 @@ public class LinearArith {
     ExprManager em = new ExprManager();
     SmtEngine smt = new SmtEngine(em);
 
-    smt.setOption("incremental", new SExpr(true)); // Enable incremental solving
-    smt.setLogic("QF_LIRA");                       // Set the logic
+    smt.setLogic("QF_LIRA"); // Set the logic
 
     // Prove that if given x (Integer) and y (Real) then
     // the maximum value of y - x is 2/3
diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java
index 2e72edf24..de71eb769 100644
--- a/examples/api/java/PipedInput.java
+++ b/examples/api/java/PipedInput.java
@@ -26,7 +26,6 @@ public class PipedInput {
     // Boilerplate setup for CVC4
     ExprManager exprMgr = new ExprManager();
     SmtEngine smt = new SmtEngine(exprMgr);
-    smt.setOption("incremental", new SExpr(true));
     smt.setOption("output-language", new SExpr("smt2"));
 
     // Set up a pair of connected Java streams
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 1c1c439df..87f9d8a5b 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -26,8 +26,7 @@ using namespace CVC4;
 int main() {
   ExprManager em;
   SmtEngine smt(&em);
-  smt.setOption("incremental", true); // Enable incremental solving
-  smt.setLogic("QF_LIRA");            // Set the logic
+  smt.setLogic("QF_LIRA"); // Set the logic
 
   // Prove that if given x (Integer) and y (Real) then
   // the maximum value of y - x is 2/3