Skip to content

Commit 120c2c6

Browse files
author
BaierD
committed
Switch int return to bool return for boolean Mathsat5 5 native call in the wrapper
1 parent 08c5594 commit 120c2c6

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -158,10 +158,10 @@ PROOF_ARG(1)
158158
CALL1(const char *, proof_get_name)
159159
PLAIN_CONST_STRING_RETURN
160160

161-
DEFINE_FUNC(int, 1proof_1is_1term) WITH_ONE_ARG(jproof)
161+
DEFINE_FUNC(jboolean, 1proof_1is_1term) WITH_ONE_ARG(jproof)
162162
PROOF_ARG(1)
163163
CALL1(int, proof_is_term)
164-
INT_RETURN
164+
BOOLEAN_RETURN
165165

166166
DEFINE_FUNC(jterm, 1proof_1get_1term) WITH_ONE_ARG(jproof)
167167
PROOF_ARG(1)

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java

-1
Original file line numberDiff line numberDiff line change
@@ -1095,7 +1095,6 @@ private static native int msat_all_sat(
10951095

10961096
public static native String msat_proof_get_name(long proof);
10971097

1098-
// Non-zero if term, 0 for no term
10991098
public static native boolean msat_proof_is_term(long proof);
11001099

11011100
// Term representation of the current proof

0 commit comments

Comments
 (0)