[info] Loading global plugins from /home/kyle/.sbt/0.13/plugins [info] Loading project definition from /home/kyle/work/dd-research/scala-smtlib/project [info] Set current project to scala-smtlib (in build file:/home/kyle/work/dd-research/scala-smtlib/) [info] ProcessInterpreterTests: [info] - Interrupt after free does not throw an exception [info] - Interrupt can be called multiple times safely [info] SmtLibRunnerTests: [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/a20test0001.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/a20test0001.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond1.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond1.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/PEQ011_size5.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/PEQ011_size5.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/NEQ046_size3.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/NEQ046_size3.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/PEQ012_size3.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/PEQ012_size3.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/quaternion_ds1_symm_0818.fof.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/quaternion_ds1_symm_0818.fof.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/bf7.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/bf7.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/broken.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/broken.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/array_free.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/array_free.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/cl5_nebula_array_0001.fof.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/cl5_nebula_array_0001.fof.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond3.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond3.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond2.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/eq_diamond2.smt2 *** FAILED *** [info] java.io.IOException: Broken pipe [info] at java.io.FileOutputStream.writeBytes(Native Method) [info] at java.io.FileOutputStream.write(FileOutputStream.java:326) [info] at java.io.BufferedOutputStream.flushBuffer(BufferedOutputStream.java:82) [info] at java.io.BufferedOutputStream.flush(BufferedOutputStream.java:140) [info] at sun.nio.cs.StreamEncoder.implFlush(StreamEncoder.java:297) [info] at sun.nio.cs.StreamEncoder.flush(StreamEncoder.java:141) [info] at java.io.OutputStreamWriter.flush(OutputStreamWriter.java:229) [info] at java.io.BufferedWriter.flush(BufferedWriter.java:254) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:13) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/b159test0001.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/b159test0001.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/SEQ004_size5.smt2 [info] - With CVC4: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/all/SEQ004_size5.smt2 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.SmtLibRunnerTests.getCVC4Interpreter(SmtLibRunnerTests.scala:24) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] at smtlib.it.SmtLibRunnerTests$$anonfun$2$$anonfun$apply$4.apply(SmtLibRunnerTests.scala:34) [info] ... [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/NEQ016_size7.smt2 [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/NEQ004_size5.smt2 [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/PEQ010_size7.smt2 [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/cmu-model15.smt2 [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/NEQ006_size4.smt2 [info] - With Z3: SMTLIB benchmark: /home/kyle/work/dd-research/scala-smtlib/target/scala-2.11/it-classes/regression/smtlib/solving/z3/PEQ002_size5.smt2 [info] TheoriesBuilderTests: [info] - 1 - Theory of Ints: with Z3 [info] - 1 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 2 - Theory of Ints: with Z3 [info] - 2 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 3 - Theory of Ints: with Z3 [info] - 3 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 4 - Theory of Ints: with Z3 [info] - 4 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 5 - Theory of Ints: with Z3 [info] - 5 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 6 - Theory of Ints: with Z3 [info] - 6 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 7 - Theory of Ints: with Z3 [info] - 7 - Theory of Ints: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 1 - Theory of Reals: with Z3 [info] - 1 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 2 - Theory of Reals: with Z3 [info] - 2 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 3 - Theory of Reals: with Z3 [info] - 3 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 4 - Theory of Reals: with Z3 [info] - 4 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 5 - Theory of Reals: with Z3 [info] - 5 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 6 - Theory of Reals: with Z3 [info] - 6 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 7 - Theory of Reals: with Z3 [info] - 7 - Theory of Reals: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 1 - Theory of Bit Vectors: with Z3 [info] - 1 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 2 - Theory of Bit Vectors: with Z3 [info] - 2 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 3 - Theory of Bit Vectors: with Z3 [info] - 3 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 4 - Theory of Bit Vectors: with Z3 [info] - 4 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 5 - Theory of Bit Vectors: with Z3 [info] - 5 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 6 - Theory of Bit Vectors: with Z3 [info] - 6 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 7 - Theory of Bit Vectors: with Z3 [info] - 7 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 8 - Theory of Bit Vectors: with Z3 [info] - 8 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 9 - Theory of Bit Vectors: with Z3 [info] - 9 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 10 - Theory of Bit Vectors: with Z3 [info] - 10 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] - 11 - Theory of Bit Vectors: with Z3 [info] - 11 - Theory of Bit Vectors: with CVC4 *** FAILED *** [info] smtlib.parser.Parser$UnexpectedEOFException: Unexpected end of file. Expected: [OParen] [info] at smtlib.parser.ParserCommon$class.check(ParserCommon.scala:90) [info] at smtlib.parser.Parser.check(Parser.scala:8) [info] at smtlib.parser.ParserCommandsResponses$class.parseGenResponse(ParserCommandsResponses.scala:31) [info] at smtlib.parser.Parser.parseGenResponse(Parser.scala:8) [info] at smtlib.interpreters.CVC4Interpreter.(CVC4Interpreter.scala:14) [info] at smtlib.interpreters.CVC4Interpreter$.buildDefault(CVC4Interpreter.scala:42) [info] at smtlib.it.TestHelpers$class.getCVC4Interpreter(TestHelpers.scala:45) [info] at smtlib.it.TheoriesBuilderTests.getCVC4Interpreter(TheoriesBuilderTests.scala:19) [info] at smtlib.it.TheoriesBuilderTests$$anonfun$mkTest$2.apply(TheoriesBuilderTests.scala:39) [info] at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85) [info] ... [info] Run completed in 14 seconds, 165 milliseconds. [info] Total number of tests run: 86 [info] Suites: completed 3, aborted 0 [info] Tests: succeeded 47, failed 39, canceled 0, ignored 0, pending 0 [info] *** 39 TESTS FAILED *** [error] Failed tests: [error] smtlib.it.TheoriesBuilderTests [error] smtlib.it.SmtLibRunnerTests [error] (it:test) sbt.TestsFailedException: Tests unsuccessful [error] Total time: 16 s, completed May 24, 2018 1:50:31 AM