Fixing a null pointer dereference in the cvc3 compatibility layer. (#1089)

2 files changed, 36 insertions, 36 deletions

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 1b38a4c95..9289a8ae7 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -160,23 +160,23 @@ public class ValidityChecker extends Embedded {
     private static native Object
 	jniCreateOp2(Object ValidityChecker, String name, Object Type, Object ExprDef) throws Cvc3Exception;
     private static native Object
-	jniEqOp() throws Cvc3Exception;
+	jniEqOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniLtOp() throws Cvc3Exception;
+	jniLtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniLeOp() throws Cvc3Exception;
+	jniLeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniGtOp() throws Cvc3Exception;
+	jniGtOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniGeOp() throws Cvc3Exception;
+	jniGeOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniPlusOp() throws Cvc3Exception;
+	jniPlusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniMinusOp() throws Cvc3Exception;
+	jniMinusOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniMultOp() throws Cvc3Exception;
+	jniMultOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
-	jniDivideOp() throws Cvc3Exception;
+	jniDivideOp(Object ValidityChecker) throws Cvc3Exception;
     private static native Object
 	jniFunExpr1(Object ValidityChecker, Object Op, Object Expr) throws Cvc3Exception;
     private static native Object
@@ -919,47 +919,47 @@ public class ValidityChecker extends Embedded {
 
     // '='
     public OpMut eqOp() throws Cvc3Exception {
-	return new OpMut(jniEqOp(), embeddedManager());
+	return new OpMut(jniEqOp(embedded()), embeddedManager());
     }
 
     // '<'
     public OpMut ltOp() throws Cvc3Exception {
-	return new OpMut(jniLtOp(), embeddedManager());
+	return new OpMut(jniLtOp(embedded()), embeddedManager());
     }
 
     // '<='
     public OpMut leOp() throws Cvc3Exception {
-	return new OpMut(jniLeOp(), embeddedManager());
+	return new OpMut(jniLeOp(embedded()), embeddedManager());
     }
 
     // '>'
     public OpMut gtOp() throws Cvc3Exception {
-	return new OpMut(jniGtOp(), embeddedManager());
+	return new OpMut(jniGtOp(embedded()), embeddedManager());
     }
 
     // '>='
     public OpMut geOp() throws Cvc3Exception {
-	return new OpMut(jniGeOp(), embeddedManager());
+	return new OpMut(jniGeOp(embedded()), embeddedManager());
     }
 
     // '+'
     public OpMut plusOp() throws Cvc3Exception {
-	return new OpMut(jniPlusOp(), embeddedManager());
+	return new OpMut(jniPlusOp(embedded()), embeddedManager());
     }
 
     // '-'
     public OpMut minusOp() throws Cvc3Exception {
-	return new OpMut(jniMinusOp(), embeddedManager());
+	return new OpMut(jniMinusOp(embedded()), embeddedManager());
     }
 
     // '*'
     public OpMut multOp() throws Cvc3Exception {
-	return new OpMut(jniMultOp(), embeddedManager());
+	return new OpMut(jniMultOp(embedded()), embeddedManager());
     }
 
     // '/' for rationals
     public OpMut divideOp() throws Cvc3Exception {
-	return new OpMut(jniDivideOp(), embeddedManager());
+	return new OpMut(jniDivideOp(embedded()), embeddedManager());
     }
 
     public ExprMut funExpr(Op op, Expr expr1) throws Cvc3Exception {
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index cfda940d8..6c6a9f8cb 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -300,40 +300,40 @@ jobject m ValidityChecker vc n string name c Type type c Expr expr
 return embed_copy(env, vc->createOp(name, *type, *expr));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniEqOp
-jobject
-return embed_copy<Op>(env, Op(EQ));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), EQ));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLtOp
-jobject
-return embed_copy<Op>(env, Op(LT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniLeOp
-jobject
-return embed_copy<Op>(env, Op(LE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), LE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGtOp
-jobject
-return embed_copy<Op>(env, Op(GT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniGeOp
-jobject
-return embed_copy<Op>(env, Op(GE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), GE));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniPlusOp
-jobject
-return embed_copy<Op>(env, Op(PLUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), PLUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMinusOp
-jobject
-return embed_copy<Op>(env, Op(MINUS));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MINUS));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniMultOp
-jobject
-return embed_copy<Op>(env, Op(MULT));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), MULT));
 
 DEFINITION: Java_cvc3_ValidityChecker_jniDivideOp
-jobject
-return embed_copy<Op>(env, Op(DIVIDE));
+jobject m ValidityChecker vc
+return embed_copy<Op>(env, Op(vc->getEM(), DIVIDE));
 
 
 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr1