OpenSMT: Removed patch that fixed the formating of printed OpenSMT fo…

…rmulas and fixed our own test. See discussion in usi-verification-and-security/opensmt#646 (comment) for details.

lib/native/source/opensmt/api.patch

@@ -258,23 +258,6 @@ index b90430c2..c4b34fc4 100644
      return mkUninterpFun(sym, std::move(terms));
  }
 
-@@ -1346,14 +1339,14 @@ void Logic::dumpWithLets(std::ostream & dump_out, PTRef formula) const {
-         if (term.size() > 0) dump_out << ")";
-
-         // Closes binding
--        dump_out << "))\n";
-+        dump_out << ")) ";
-         // Keep track of number of lets to close
-         num_lets++;
-
-         assert(enode_to_def.find(e) == enode_to_def.end());
-         enode_to_def[e] = std::move(definition);
-     }
--    dump_out << '\n' << enode_to_def[formula] << '\n';
-+    dump_out << enode_to_def[formula];
-
-     // Close all lets
-     for (unsigned n = 1; n <= num_lets; n++) dump_out << ")";
 @@ -1488,6 +1481,9 @@ Logic::collectStats(PTRef root, int& n_of_conn, int& n_of_eq, int& n_of_uf, int&
 
  PTRef Logic::conjoinExtras(PTRef root) { return root; }

src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java

@@ -409,6 +409,10 @@ private void checkThatFunOnlyDeclaredOnce(String formDump) {
   private void checkThatAssertIsInLastLine(String lines) {
     // Boolector will fail this anyway since bools are bitvecs for btor
     TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
+
+    // OpenSMT has newline characters within the (assert ..) block that break this test
+    TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.OPENSMT);
+
     lines = lines.trim();
     assertWithMessage("last line of <\n" + lines + ">")
         .that(getLast(Splitter.on('\n').split(lines)))