Remove hack for CVC4

CVC4 1.6 fixed the bug with multiple success on define-funs-rec
so I remove that hack from the Interpreter. The CVC4Interpreter will
only work with a recent version of CVC4 though, but I don't want to
support multiple versions anyway. We can also drop some flags.

Go around another CVC4 bug by removing some empty lines in set-source
lines, see issue regb#31 for details.

Author: regb

src/it/resources/regression/smtlib/solving/all/a20test0001.smt2

@@ -3,9 +3,7 @@
 (set-info :source |
 Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
 ([email protected]).  Translated into SMT-LIB format by Clark Barrett using
-CVC3.
-
-|)
+CVC3.  |)
 (set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)

src/it/resources/regression/smtlib/solving/all/array_free.smt2

@@ -5,8 +5,7 @@
 (set-info :category "industrial")
 (set-info :source |
   Generated using using the Low-Level Bounded Model Checker LLBMC.
-  C files used in the paper: Florian Merz, Stephan Falke, Carsten Sinz: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. VSTTE 2012: 146-161
-|)
+  C files used in the paper: Florian Merz, Stephan Falke, Carsten Sinz: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. VSTTE 2012: 146-161 |)
 (declare-fun initialMemoryState_0x228bd90 () (Array (_ BitVec 64) (_ BitVec 8)))
 (assert
 (let ((?x1 (_ bv0 8)))

src/it/resources/regression/smtlib/solving/all/b159test0001.smt2

@@ -3,9 +3,7 @@
 (set-info :source |
 Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
 ([email protected]).  Translated into SMT-LIB format by Clark Barrett using
-CVC3.
-
-|)
+CVC3.  |)
 (set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)

src/it/resources/regression/smtlib/solving/all/bf7.smt2

@@ -5,8 +5,7 @@
 (set-info :category "industrial")
 (set-info :source |
   Generated using using the Low-Level Bounded Model Checker LLBMC.
-  C files used in the paper: Florian Merz, Stephan Falke, Carsten Sinz: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. VSTTE 2012: 146-161
-|)
+  C files used in the paper: Florian Merz, Stephan Falke, Carsten Sinz: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. VSTTE 2012: 146-161 |)
 (declare-fun initialMemoryState_0x1e97470 () (Array (_ BitVec 64) (_ BitVec 8)))
 (assert
 (let ((?x1 (_ bv0 32)))

src/it/resources/regression/smtlib/solving/all/broken.smt2

@@ -3,9 +3,7 @@
 (set-info :source |
 Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh
 ([email protected]).  Translated into SMT-LIB format by Clark Barrett using
-CVC3.
-
-|)
+CVC3.  |)
 (set-info :smt-lib-version 2.0)
 (set-info :category "industrial")
 (set-info :status sat)

src/it/scala/smtlib/it/TestHelpers.scala

@@ -65,7 +65,7 @@ trait TestHelpers {
   }
 
   def executeCVC4(file: File)(f: (String) => Unit): Unit = {
-    Seq("cvc4", "--lang", "smt", "--incremental", "--produce-models", file.getPath) ! ProcessLogger(f, s => ())
+    Seq("cvc4", "--lang", "smt", file.getPath) ! ProcessLogger(f, s => ())
   }
 
 }

src/main/scala/smtlib/interpreters/CVC4Interpreter.scala

@@ -13,28 +13,6 @@ class CVC4Interpreter(executable: String, args: Array[String], tailPrinter: Bool
   in.flush
   parser.parseGenResponse
 
-  override def parseResponseOf(cmd: SExpr): SExpr = cmd match {
-    case DefineFunsRec(funs, _) =>
-      // CVC4 translates define-funs-rec in three commands per function,
-      // and thus emits 3x success.
-      val res = for (i <- 1 to funs.size*3) yield {
-        parser.parseGenResponse
-      }
-
-      res.find(_ != Success).getOrElse(Success)
-
-    case DefineFunRec(_) =>
-      // CVC4 translates define-fun-rec in three commands,
-      // and thus emits 3x success.
-      val res = for (i <- 1 to 3) yield {
-        parser.parseGenResponse
-      }
-
-      res.find(_ != Success).getOrElse(Success)
-
-    case _ =>
-      super.parseResponseOf(cmd)
-  }
 }
 
 object CVC4Interpreter {