From 2f35236924fbffca12c0fa35c1b947494d340c13 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 9 Mar 2026 18:10:33 +0100 Subject: [PATCH 1/8] Update constructors and yval tags with new entries for finite fields We're not adding the entire ff API, but just the new constructors. This was necessary as the new constructors changed the values of existing constructors Adding the rest of the API will have to be done in a separate commit See https://github.com/SRI-CSL/yices2/pull/605 --- src/main/java/com/sri/yices/Constructor.java | 86 ++++++++++---------- src/main/java/com/sri/yices/YValTag.java | 1 + 2 files changed, 45 insertions(+), 42 deletions(-) diff --git a/src/main/java/com/sri/yices/Constructor.java b/src/main/java/com/sri/yices/Constructor.java index 665436b..9e3bc70 100644 --- a/src/main/java/com/sri/yices/Constructor.java +++ b/src/main/java/com/sri/yices/Constructor.java @@ -11,64 +11,66 @@ public enum Constructor { // atomic terms BOOL_CONSTANT(0), // boolean constant ARITH_CONSTANT(1), // rational constant - BV_CONSTANT(2), // bitvector constant - SCALAR_CONSTANT(3), // constant of uninterpreted or scalar type - VARIABLE(4), // variable in quantifiers - UNINTERPRETED_TERM(5), // (i.e., global variables, can't be bound) + FF_CONSTANT(2), // finite field constant + BV_CONSTANT(3), // bitvector constant + SCALAR_CONSTANT(4), // constant of uninterpreted or scalar type + VARIABLE(5), // variable in quantifiers + UNINTERPRETED_TERM(6), // (i.e., global variables, can't be bound) // composite terms - ITE_TERM(6), // if-then-else - APP_TERM(7), // application of an uninterpreted function - UPDATE_TERM(8), // function update - TUPLE_TERM(9), // tuple constructor - EQ_TERM(10), // equality - DISTINCT_TERM(11), // distinct t_1 ... t_n - FORALL_TERM(12), // quantifier - LAMBDA_TERM(13), // lambda - NOT_TERM(14), // (not t) - OR_TERM(15), // n-ary OR - XOR_TERM(16), // n-ary XOR + ITE_TERM(7), // if-then-else + APP_TERM(8), // application of an uninterpreted function + UPDATE_TERM(9), // function update + TUPLE_TERM(10), // tuple constructor + EQ_TERM(11), // equality + DISTINCT_TERM(12), // distinct t_1 ... t_n + FORALL_TERM(13), // quantifier + LAMBDA_TERM(14), // lambda + NOT_TERM(15), // (not t) + OR_TERM(16), // n-ary OR + XOR_TERM(17), // n-ary XOR - BV_ARRAY(17), // array of boolean terms - BV_DIV(18), // unsigned division - BV_REM(19), // unsigned remainder - BV_SDIV(20), // signed division - BV_SREM(21), // remainder in signed division (rounding to 0) - BV_SMOD(22), // remainder in signed division (rounding to -infinity) - BV_SHL(23), // shift left (padding with 0) - BV_LSHR(24), // logical shift right (padding with 0) - BV_ASHR(25), // arithmetic shift right (padding with sign bit) - BV_GE_ATOM(26), // unsigned comparison: (t1 >= t2) - BV_SGE_ATOM(27), // signed comparison (t1 >= t2) - ARITH_GE_ATOM(28), // atom (t1 >= t2) for arithmetic terms: t2 is always 0 - ARITH_ROOT_ATOM(29), // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >= + BV_ARRAY(18), // array of boolean terms + BV_DIV(19), // unsigned division + BV_REM(20), // unsigned remainder + BV_SDIV(21), // signed division + BV_SREM(22), // remainder in signed division (rounding to 0) + BV_SMOD(23), // remainder in signed division (rounding to -infinity) + BV_SHL(24), // shift left (padding with 0) + BV_LSHR(25), // logical shift right (padding with 0) + BV_ASHR(26), // arithmetic shift right (padding with sign bit) + BV_GE_ATOM(27), // unsigned comparison: (t1 >= t2) + BV_SGE_ATOM(28), // signed comparison (t1 >= t2) + ARITH_GE_ATOM(29), // atom (t1 >= t2) for arithmetic terms: t2 is always 0 + ARITH_ROOT_ATOM(30), // atom (0 <= k <= root_count(p)) && (x r root(p, k)) for r in <, <=, ==, !=, >, >= - ABS(30), // absolute value - CEIL(31), // ceil - FLOOR(32), // floor - RDIV(33), // real division (as in x/y) - IDIV(34), // integer division - IMOD(35), // modulo - IS_INT_ATOM(36), // integrality test: (is-int t) - DIVIDES_ATOM(37), // divisibility test: (divides t1 t2) + ABS(31), // absolute value + CEIL(32), // ceil + FLOOR(33), // floor + RDIV(34), // real division (as in x/y) + IDIV(35), // integer division + IMOD(36), // modulo + IS_INT_ATOM(37), // integrality test: (is-int t) + DIVIDES_ATOM(38), // divisibility test: (divides t1 t2) // projections - SELECT_TERM(38), // tuple projection - BIT_TERM(39), // bit-select: extract the i-th bit of a bitvector + SELECT_TERM(39), // tuple projection + BIT_TERM(40), // bit-select: extract the i-th bit of a bitvector // sums - BV_SUM(40), // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term) - ARITH_SUM(41), // sum of pairs a * t where a is a rational (and t is an arithmetic term) + BV_SUM(41), // sum of pairs a * t where a is a bitvector constant (and t is a bitvector term) + ARITH_SUM(42), // sum of pairs a * t where a is a rational (and t is an arithmetic term) + FF_SUM(43), // sum of pairs a * t where a is a finite-field constant (and t is a finite-field term) // products - POWER_PRODUCT(42) // power products: (t1^d1 * ... * t_n^d_n) + POWER_PRODUCT(44) // power products: (t1^d1 * ... * t_n^d_n) ; private int index; Constructor(int id) { this.index = id; } public int getIndex() { return index; } - public static final int NUM_CONSTRUCTORS = 43; + public static final int NUM_CONSTRUCTORS = 45; private static final Constructor[] table; static { diff --git a/src/main/java/com/sri/yices/YValTag.java b/src/main/java/com/sri/yices/YValTag.java index eb43561..a960762 100644 --- a/src/main/java/com/sri/yices/YValTag.java +++ b/src/main/java/com/sri/yices/YValTag.java @@ -13,6 +13,7 @@ public enum YValTag { BOOL, RATIONAL, ALGEBRAIC, + FINITEFIELD, BV, SCALAR, TUPLE, From 572c4cda3b187d03c9e4b4faf8bf0f7af2ac009f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 9 Mar 2026 18:12:46 +0100 Subject: [PATCH 2/8] Update names of SAT status constants --- src/main/java/com/sri/yices/yicesJNI.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp index 27290e2..46a4a9a 100644 --- a/src/main/java/com/sri/yices/yicesJNI.cpp +++ b/src/main/java/com/sri/yices/yicesJNI.cpp @@ -3215,10 +3215,10 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkContextWithInterpolation(JN ctx.model = NULL; try { result = yices_check_context_with_interpolation(&ctx, reinterpret_cast(params), build_model); - if (result == STATUS_UNSAT) { + if (result == YICES_STATUS_UNSAT) { // set the interpolant array env->SetIntArrayRegion(interpolant, 0, 1, &ctx.interpolant); - } else if(build_model && result == STATUS_SAT ) { + } else if(build_model && result == YICES_STATUS_SAT ) { model_t *model = ctx.model; jlong mdl = reinterpret_cast(model); // set the model array @@ -3817,7 +3817,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormula(JNIEnv *env, jclass } if (wantModel) { code = yices_check_formula(formula, ls, &model, ds); - if (code == STATUS_SAT) { + if (code == YICES_STATUS_SAT) { mdl = reinterpret_cast(model); env->SetLongArrayRegion(marr, 0, 1, &mdl); } @@ -3873,7 +3873,7 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_checkFormulas(JNIEnv *env, jclas } if (wantModel) { code = yices_check_formulas(tarr, n, ls, &model, ds); - if (code == STATUS_SAT) { + if (code == YICES_STATUS_SAT) { mdl = reinterpret_cast(model); env->SetLongArrayRegion(marr, 0, 1, &mdl); } From a7d10fbef51b043c3c606131557c9c227c303106 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 9 Mar 2026 18:16:11 +0100 Subject: [PATCH 3/8] Allow Parameters argument to be "null" --- src/main/java/com/sri/yices/Context.java | 4 ++-- src/main/java/com/sri/yices/InterpolationContext.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/java/com/sri/yices/Context.java b/src/main/java/com/sri/yices/Context.java index 53ac5b6..6803df5 100644 --- a/src/main/java/com/sri/yices/Context.java +++ b/src/main/java/com/sri/yices/Context.java @@ -331,7 +331,7 @@ public int getModelInterpolant() { // Since 2.6.4 public Status checkWithAssumptions(Parameters params, int[] assumptions) { - int code = Yices.checkContextWithAssumptions(ptr, params.getPtr(), assumptions); + int code = Yices.checkContextWithAssumptions(ptr, params == null ? 0 : params.getPtr(), assumptions); if (code < 0) { throw new YicesException(); } @@ -340,7 +340,7 @@ public Status checkWithAssumptions(Parameters params, int[] assumptions) { // Since 2.6.4 public Status checkWithModel(Parameters params, Model model, int[] assumptions) { - int code = Yices.checkContextWithModel(ptr, params.getPtr(), model.getPtr(), assumptions); + int code = Yices.checkContextWithModel(ptr, params == null ? 0 : params.getPtr(), model.getPtr(), assumptions); if (code < 0) { YicesException error = YicesException.checkVersion(2, 6, 4); if (error == null) { diff --git a/src/main/java/com/sri/yices/InterpolationContext.java b/src/main/java/com/sri/yices/InterpolationContext.java index 2865ed5..d1a1e8a 100644 --- a/src/main/java/com/sri/yices/InterpolationContext.java +++ b/src/main/java/com/sri/yices/InterpolationContext.java @@ -35,7 +35,7 @@ public Status check(Parameters params, boolean buildModel) { int[] tarr = { 0 }; long[] marr = { 0 }; if (!buildModel) { marr = null; } - int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params.getPtr(), marr, tarr); + int code = Yices.checkContextWithInterpolation(this.ctxA.getPtr(), this.ctxB.getPtr(), params == null ? 0 : params.getPtr(), marr, tarr); Status status = Status.idToStatus(code); if (status == Status.ERROR) { throw new YicesException(); From 8a5ac3bc150b25024970842f1c9874c08a72fc2e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 9 Mar 2026 18:19:41 +0100 Subject: [PATCH 4/8] Make checks for `Model.expandFuntion` less strict Yices may return zero mappings for a function if it is constant (f.ex `f(x)=0`) --- src/main/java/com/sri/yices/Model.java | 2 +- src/main/java/com/sri/yices/yicesJNI.cpp | 13 ++++--------- 2 files changed, 5 insertions(+), 10 deletions(-) diff --git a/src/main/java/com/sri/yices/Model.java b/src/main/java/com/sri/yices/Model.java index bcd710f..5cbab09 100644 --- a/src/main/java/com/sri/yices/Model.java +++ b/src/main/java/com/sri/yices/Model.java @@ -398,7 +398,7 @@ public YVal[] expandTuple(YVal yval) throws YicesException { public VectorValue expandFunction(YVal yval) throws YicesException { int n = Yices.valFunctionCardinality(ptr, yval.tag.ordinal(), yval.id); - if (n <= 0) throw new YicesException(); + if (n < 0) throw new YicesException(); YVal[] vector = new YVal[n]; YVal[] value = new YVal[1]; int code = Yices.valExpandFunction(ptr, yval.tag.ordinal(), yval.id, value, vector); diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp index 46a4a9a..4a9a0a1 100644 --- a/src/main/java/com/sri/yices/yicesJNI.cpp +++ b/src/main/java/com/sri/yices/yicesJNI.cpp @@ -4577,7 +4577,6 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valFunctionCardinality(JNIEnv *e JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, jclass cls, jlong mdl, jint tag, jint id, jobjectArray def, jobjectArray mappings){ yval_t yval; int32_t cardinality; - jsize ndef; jsize nmap; int32_t code; yval_t ydef; @@ -4588,22 +4587,18 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_valExpandFunction(JNIEnv *env, j return -1; } cardinality = Java_com_sri_yices_Yices_valFunctionCardinality(env, cls, mdl, tag, id); - if (cardinality <= 0) { - return -2; - } - ndef = env->GetArrayLength(def); - if (ndef < 1) { - return -3; + if (cardinality < 0) { + return -1; } nmap = env->GetArrayLength(mappings); if (nmap < cardinality) { - return -4; + return -1; } yices_init_yval_vector(&ymaps); code = yices_val_expand_function(reinterpret_cast(mdl), &yval, &ydef, &ymaps); if (code < 0) { - return -5; + return -1; } assert(static_cast(ymaps.size) == cardinality); From 2703f0f74676801fbf6962dab002c5a92108f75b Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 9 Mar 2026 18:29:16 +0100 Subject: [PATCH 5/8] Add support for sums and products Yices will rewrite terms that were built with regular (binary) addition or multiplication as sums and products. So we need these methods to access the terms, even when we're not creating sums/products ourselves --- .../java/com/sri/yices/ProductComponent.java | 19 +++ src/main/java/com/sri/yices/SumComponent.java | 19 +++ src/main/java/com/sri/yices/Terms.java | 11 ++ src/main/java/com/sri/yices/Yices.java | 43 +++++++ src/main/java/com/sri/yices/yicesJNI.cpp | 110 ++++++++++++++++++ 5 files changed, 202 insertions(+) create mode 100644 src/main/java/com/sri/yices/ProductComponent.java create mode 100644 src/main/java/com/sri/yices/SumComponent.java diff --git a/src/main/java/com/sri/yices/ProductComponent.java b/src/main/java/com/sri/yices/ProductComponent.java new file mode 100644 index 0000000..94d6b20 --- /dev/null +++ b/src/main/java/com/sri/yices/ProductComponent.java @@ -0,0 +1,19 @@ +package com.sri.yices; + +public class ProductComponent { + private final int power; + private final int term; + + public ProductComponent(int pTerm, int pPower) { + power = pPower; + term = pTerm; + } + + public int getTerm() { + return term; + } + + public int getPower() { + return power; + } +} diff --git a/src/main/java/com/sri/yices/SumComponent.java b/src/main/java/com/sri/yices/SumComponent.java new file mode 100644 index 0000000..12658de --- /dev/null +++ b/src/main/java/com/sri/yices/SumComponent.java @@ -0,0 +1,19 @@ +package com.sri.yices; + +public class SumComponent { + private final T factor; + private final int term; + + public SumComponent(T pFactor, int pTerm) { + factor = pFactor; + term = pTerm; + } + + public T getFactor() { + return factor; + } + + public int getTerm() { + return term; + } +} diff --git a/src/main/java/com/sri/yices/Terms.java b/src/main/java/com/sri/yices/Terms.java index 1f2745c..b096a27 100644 --- a/src/main/java/com/sri/yices/Terms.java +++ b/src/main/java/com/sri/yices/Terms.java @@ -1258,6 +1258,17 @@ static public int projArg(int x) throws YicesException { return t; } + static public SumComponent projSum(int x, int idx) throws YicesException { + SumComponent c = Yices.sumComponent(x, idx); + if (c == null) throw new YicesException(); + return c; + } + + static public ProductComponent projProduct(int x, int idx) throws YicesException { + ProductComponent c = Yices.productComponent(x, idx); + if (c == null) throw new YicesException(); + return c; + } /* * Check whether term x is a constant diff --git a/src/main/java/com/sri/yices/Yices.java b/src/main/java/com/sri/yices/Yices.java index cf628da..1e4f023 100644 --- a/src/main/java/com/sri/yices/Yices.java +++ b/src/main/java/com/sri/yices/Yices.java @@ -384,6 +384,49 @@ public static int mkRationalConstant(BigInteger num, BigInteger den) { public static native int termProjIndex(int x); public static native int termProjArg(int x); + public static native byte[] sumComponentNumAsBytes(int x, int idx); + public static native byte[] sumComponentDenAsBytes(int x, int idx); + public static native int sumComponentTerm(int x, int idx); + + public static native boolean[] bvSumComponentFactor(int x, int idx); + public static native int bvSumComponentTerm(int x, int idx); + + public static SumComponent sumComponent(int x, int idx) { + SumComponent result = null; + if (Yices.termIsArithmetic(x)) { + byte[] num = sumComponentNumAsBytes(x, idx); + byte[] den = sumComponentDenAsBytes(x, idx); + int term = sumComponentTerm(x, idx); + + if (num != null && den != null) { + result = new SumComponent<>(new BigRational(num, den), term); + } + } + if (Yices.termIsBitvector(x)) { + boolean[] factor = bvSumComponentFactor(x, idx); + int term = bvSumComponentTerm(x, idx); + + if (factor != null) { + result = new SumComponent<>(factor, term); + } + } + return result; + } + + public static native int productComponentTerm(int x, int idx); + public static native int productComponentPower(int x, int idx); + + public static ProductComponent productComponent(int x, int idx) { + int power = productComponentPower(x, idx); + int term = productComponentTerm(x, idx); + + if (term >= 0) { + return new ProductComponent(term, power); + } else { + return null; + } + } + /* * Values of constant terms * To access the value of rational constants, we provide two functions: diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp index 4a9a0a1..6e7fca8 100644 --- a/src/main/java/com/sri/yices/yicesJNI.cpp +++ b/src/main/java/com/sri/yices/yicesJNI.cpp @@ -2630,6 +2630,116 @@ JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_termProjArg(JNIEnv *env, jclass, return yices_proj_arg(x); } +JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentNumAsBytes(JNIEnv *env, jclass, jint x, jint idx) { + jbyteArray result = NULL; + mpq_t q; + jint t = -1; + + mpq_init(q); + if (yices_sum_component(x, idx, q, &t) >= 0) { + result = mpz_to_byte_array(env, mpq_numref(q)); + } + mpq_clear(q); + + return result; +} + +JNIEXPORT jbyteArray JNICALL Java_com_sri_yices_Yices_sumComponentDenAsBytes(JNIEnv *env, jclass, jint x, jint idx) { + jbyteArray result = NULL; + mpq_t q; + jint t = -1; + + mpq_init(q); + if (yices_sum_component(x, idx, q, &t) >= 0) { + result = mpz_to_byte_array(env, mpq_denref(q)); + } + mpq_clear(q); + + return result; +} + +JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_sumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) { + jint result; + mpq_t q; + + mpq_init(q); + yices_sum_component(x, idx, q, &result); + mpq_clear(q); + + return result; +} + +JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvSumComponentFactor(JNIEnv *env, jclass, jint x, jint idx) { + jbooleanArray result = NULL; + jint t = -1; + + int32_t n = yices_term_bitsize(x); + assert(n >= 0); + + if (n <= 64) { + // this should be the common case + int32_t a[64]; + int32_t code = yices_bvsum_component(x, idx, a, &t); + assert(code >= 0); + result = convertToBoolArray(env, n, a); + + } else { + try { + int32_t *tmp = new int32_t[n]; + int32_t code = yices_bvsum_component(x, idx, tmp, &t); + assert(code >= 0); + result = convertToBoolArray(env, n, tmp); + delete [] tmp; + } catch (std::bad_alloc&) { + out_of_mem_exception(env); + } + } + + return result; +} + +JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_bvSumComponentTerm(JNIEnv *env, jclass, jint x, jint idx) { + jint result = -1; + + int32_t n = yices_term_bitsize(x); + assert(n >= 0); + + if (n <= 64) { + // this should be the common case + int32_t a[64]; + int32_t code = yices_bvsum_component(x, idx, a, &result); + assert(code >= 0); + + } else { + try { + int32_t *tmp = new int32_t[n]; + int32_t code = yices_bvsum_component(x, idx, tmp, &result); + assert(code >= 0); + delete [] tmp; + } catch (std::bad_alloc&) { + out_of_mem_exception(env); + } + } + + return result; +} + +JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentTerm(JNIEnv *env, jclass, jint x, jint idx) { + uint32_t p = 0; + jint t = -1; + + yices_product_component(x, idx, &t, &p); + return t; +} + +JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_productComponentPower(JNIEnv *env, jclass, jint x, jint idx) { + uint32_t p = 0; + jint t = -1; + + yices_product_component(x, idx, &t, &p); + return p; +} + JNIEXPORT jint JNICALL Java_com_sri_yices_Yices_boolConstValue(JNIEnv *env, jclass, jint x) { int32_t val; jint result; From 8fbd3a508828bbf81d72387857d9aa1e6f7fdf2f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 13 Mar 2026 17:04:57 +0100 Subject: [PATCH 6/8] Fix JNI compile warning --- src/main/java/com/sri/yices/yicesJNI.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp index 6e7fca8..03b8e30 100644 --- a/src/main/java/com/sri/yices/yicesJNI.cpp +++ b/src/main/java/com/sri/yices/yicesJNI.cpp @@ -2784,7 +2784,7 @@ JNIEXPORT jbooleanArray JNICALL Java_com_sri_yices_Yices_bvConstValue(JNIEnv *en assert(code >= 0); result = convertToBoolArray(env, n, tmp); delete [] tmp; - } catch (std::bad_alloc) { + } catch (std::bad_alloc&) { out_of_mem_exception(env); } } From 06099613527fc80461694797873cd6b5454fe799 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 14 Mar 2026 18:56:42 +0100 Subject: [PATCH 7/8] Add an option to skip loading the library Set the system property 'yices.skipAutoloader' to 'true' if the binary has already been preloaded --- src/main/java/com/sri/yices/Yices.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/main/java/com/sri/yices/Yices.java b/src/main/java/com/sri/yices/Yices.java index 1e4f023..ea39201 100644 --- a/src/main/java/com/sri/yices/Yices.java +++ b/src/main/java/com/sri/yices/Yices.java @@ -13,7 +13,10 @@ public final class Yices { */ static { try { - System.loadLibrary("yices2java"); + String skip = System.getProperty("yices.skipAutoloader", "false"); + if (!Boolean.parseBoolean(skip)) { + System.loadLibrary("yices2java"); + } init(); is_ready = true; } catch (LinkageError e) { From 0f92154e9f517de638e5717e3de3d36343c2a8a5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 17 Mar 2026 07:57:07 +0100 Subject: [PATCH 8/8] Abort if `make` fails With failifexecutionfails the build only fails if the `make` command can't be found. We should use failonerror instead, and abort if `make` has returned an error --- build.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/build.xml b/build.xml index 8dceaf6..e77e7b6 100644 --- a/build.xml +++ b/build.xml @@ -223,7 +223,7 @@ Executing "make ${library}" in ${code} + failonerror="true"> @@ -233,7 +233,7 @@ + failonerror="true"> @@ -250,7 +250,7 @@ + failonerror="true">