Java datatype API fixups, datatype API examples

2 files changed, 7 insertions, 7 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ec37eaf26..f26456cae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2506,7 +2506,7 @@ void SmtEnginePrivate::doMiplibTrick() {
         const uint64_t mark = (*j).second;
         const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
         uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
-        expected = (expected == 0) ? -1 : expected;// fix for overflow
+        expected = (expected == 0) ? -1 : expected; // fix for overflow
         Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl;
         Assert(pos.getKind() == kind::AND || pos.isVar());
         if(mark != expected) {
@@ -2514,7 +2514,7 @@ void SmtEnginePrivate::doMiplibTrick() {
         } else {
           if(mark != 3) { // exclude single-var case; nothing to check there
             uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
-            sz = (sz == 0) ? -1 : sz;// fix for overflow
+            sz = (sz == 0) ? -1 : sz; // fix for overflow
             Assert(sz == mark, "expected size %u == mark %u", sz, mark);
             for(size_t k = 0; k < checks[pos_var].size(); ++k) {
               if((k & (k - 1)) != 0) {
@@ -2534,12 +2534,12 @@ void SmtEnginePrivate::doMiplibTrick() {
                   break;
                 }
               } else {
-                Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str());// we never set for single-positive-var
+                Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var
               }
             }
           }
           if(!eligible) {
-            eligible = true;// next is still eligible
+            eligible = true; // next is still eligible
             continue;
           }
 
@@ -2563,7 +2563,7 @@ void SmtEnginePrivate::doMiplibTrick() {
               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
               d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
               SubstitutionMap nullMap(&d_fakeContext);
-              Theory::PPAssertStatus status CVC4_UNUSED;// just for assertions
+              Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
               status = d_smt.d_theoryEngine->solve(geq, nullMap);
               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
                      "unexpected solution from arith's ppAssert()");
@@ -3493,7 +3493,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
 
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
   if( options::typeChecking() ) {
-    e.getType(true);// ensure expr is type-checked at this point
+    e.getType(true); // ensure expr is type-checked at this point
   }
 
   // Make sure all preprocessing is done
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index ff4105241..00c332bd1 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -43,8 +43,8 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
   }
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
-%ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
 %ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
+%ignore CVC4::smt::currentProofManager();
 
 %include "smt/smt_engine.h"