diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..25f8fd9
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,146 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+
+permissions:
+  contents: read
+
+env:
+  FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true"
+  YICES_REF: yices-2.7.0
+
+jobs:
+  unix:
+    name: ${{ matrix.os }}
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - ubuntu-latest
+          - macos-latest
+
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Checkout Yices
+        uses: actions/checkout@v5
+        with:
+          repository: SRI-CSL/yices2
+          ref: ${{ env.YICES_REF }}
+          path: y2
+          fetch-depth: 1
+          sparse-checkout: |
+            Makefile
+            Makefile.build
+            configure
+            configure.ac
+            config.guess
+            config.sub
+            gmaketest
+            install-sh
+            make.include.in
+            autoconf
+            configs
+            scripts
+            src
+            utils
+          sparse-checkout-cone-mode: false
+
+      - name: Set up Java
+        uses: actions/setup-java@v5
+        with:
+          distribution: temurin
+          java-version: "17"
+
+      - name: Install Linux dependencies
+        if: runner.os == 'Linux'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ant autoconf automake g++ gcc gperf libgmp-dev libtool m4 make pkg-config
+
+      - name: Install macOS dependencies
+        if: runner.os == 'macOS'
+        env:
+          HOMEBREW_NO_AUTO_UPDATE: "1"
+        run: |
+          brew install ant autoconf automake gmp gperf libtool make pkg-config
+
+      - name: Build and test
+        env:
+          YICES_SRC: ${{ github.workspace }}/y2
+          YICES_PREFIX: ${{ runner.temp }}/yices-install
+        run: bash scripts/ci-build-test-unix.sh
+
+  windows:
+    name: windows-latest
+    runs-on: windows-latest
+
+    steps:
+      - run: git config --system core.longpaths true
+
+      - run: git config --global core.autocrlf false && git config --global core.eol lf
+
+      - uses: actions/checkout@v5
+
+      - name: Checkout Yices
+        uses: actions/checkout@v5
+        with:
+          repository: SRI-CSL/yices2
+          ref: ${{ env.YICES_REF }}
+          path: y2
+          fetch-depth: 1
+          sparse-checkout: |
+            Makefile
+            Makefile.build
+            configure
+            configure.ac
+            config.guess
+            config.sub
+            gmaketest
+            install-sh
+            make.include.in
+            autoconf
+            configs
+            scripts
+            src
+            utils
+          sparse-checkout-cone-mode: false
+
+      - name: Set up Java
+        uses: actions/setup-java@v5
+        with:
+          distribution: temurin
+          java-version: "17"
+
+      - name: Install Ant
+        shell: powershell
+        run: choco install ant -y
+
+      - name: Install Cygwin dependencies
+        uses: cygwin/cygwin-install-action@v4
+        with:
+          packages: |
+            autoconf,
+            automake,
+            cmake,
+            coreutils,
+            curl,
+            gperf,
+            libtool,
+            m4,
+            make,
+            mingw64-x86_64-gcc-core,
+            mingw64-x86_64-gcc-g++,
+            moreutils,
+            wget
+
+      - name: Build and test
+        shell: bash
+        env:
+          CYGWIN: winsymlinks:native binmode
+          YICES_SRC: ${{ github.workspace }}/y2
+          YICES_PREFIX: /tmp/yices-install
+        run: bash scripts/ci-build-test-windows.sh
diff --git a/ant.sh b/ant.sh
index 42b359c..5ee5d95 100755
--- a/ant.sh
+++ b/ant.sh
@@ -1,6 +1,8 @@
 #!/bin/bash
 
 #uses the build.sh to mimic what 'ant install' does without 'ant'
+set -e
+
 REPO_ROOT=${PWD}
 
 YC=${REPO_ROOT}/build/classes
@@ -8,6 +10,6 @@ YI=${REPO_ROOT}/dist/lib
 
 YICES_CLASSPATH=${YC} YICES_JNI=${YI} ./build.sh
 
-jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} ${YC}/com/sri/yices/*.class
+jar -cvfm ${YI}/yices.jar ${REPO_ROOT}/MANIFEST.txt -C ${YC} .
 
 java -Djava.library.path=${REPO_ROOT}/dist/lib -jar ${REPO_ROOT}/dist/lib/yices.jar
diff --git a/build.xml b/build.xml
index 8dceaf6..b3696ce 100644
--- a/build.xml
+++ b/build.xml
@@ -223,7 +223,7 @@
     <echo> Executing "make ${library}" in ${code} </echo>
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="${library}"/>
     </exec>
 
@@ -233,7 +233,7 @@
 
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="install"/>
     </exec>
 
@@ -250,7 +250,7 @@
 
     <exec executable="make"
           dir="${code}"
-          failifexecutionfails="true">
+          failonerror="true">
       <arg line="clean"/>
     </exec>
   </target>
@@ -286,6 +286,7 @@
       <test name="com.sri.yices.TestTypes"/>
       <test name="com.sri.yices.TestYices"/>
       <test name="com.sri.yices.TestModels"/>
+      <test name="com.sri.yices.TestTermComponents"/>
       <!-- <test name="com.sri.yices.TestDelegates"/> -->
       <!-- <test name="com.sri.yices.TestDimacs"/> -->
       <test name="com.sri.yices.TestThreads"/>
diff --git a/scripts/ci-build-test-unix.sh b/scripts/ci-build-test-unix.sh
new file mode 100644
index 0000000..cb9aa91
--- /dev/null
+++ b/scripts/ci-build-test-unix.sh
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+YICES_SRC="${YICES_SRC:?set YICES_SRC}"
+YICES_PREFIX="${YICES_PREFIX:?set YICES_PREFIX}"
+
+configure_brew_env() {
+  if [[ "$(uname)" != "Darwin" ]]; then
+    return
+  fi
+
+  local brew_prefix
+  if [[ -d /opt/homebrew ]]; then
+    brew_prefix=/opt/homebrew
+  else
+    brew_prefix=/usr/local
+  fi
+
+  export CPPFLAGS="-I${brew_prefix}/include ${CPPFLAGS:-}"
+  export LDFLAGS="-L${brew_prefix}/lib ${LDFLAGS:-}"
+  export PKG_CONFIG_PATH="${brew_prefix}/lib/pkgconfig${PKG_CONFIG_PATH:+:${PKG_CONFIG_PATH}}"
+  export DYLD_LIBRARY_PATH="${brew_prefix}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
+}
+
+build_yices() {
+  rm -rf "${YICES_PREFIX}"
+  mkdir -p "${YICES_PREFIX}"
+  pushd "${YICES_SRC}" >/dev/null
+  autoconf
+  ./configure --prefix="${YICES_PREFIX}" --enable-thread-safety --disable-mcsat
+  make MODE=release
+  make MODE=release install
+  popd >/dev/null
+}
+
+run_java_ci() {
+  export CPPFLAGS="-I${YICES_PREFIX}/include ${CPPFLAGS:-}"
+  export LDFLAGS="-L${YICES_PREFIX}/lib ${LDFLAGS:-}"
+
+  if [[ "$(uname)" == "Darwin" ]]; then
+    export DYLD_LIBRARY_PATH="${YICES_PREFIX}/lib${DYLD_LIBRARY_PATH:+:${DYLD_LIBRARY_PATH}}"
+  else
+    export LD_LIBRARY_PATH="${YICES_PREFIX}/lib${LD_LIBRARY_PATH:+:${LD_LIBRARY_PATH}}"
+  fi
+
+  export YICES_JNI="${REPO_ROOT}/dist/lib"
+  export YICES_CLASSPATH="${REPO_ROOT}/build/classes"
+
+  pushd "${REPO_ROOT}" >/dev/null
+  ant clean test
+  popd >/dev/null
+}
+
+configure_brew_env
+build_yices
+run_java_ci
diff --git a/scripts/ci-build-test-windows.sh b/scripts/ci-build-test-windows.sh
new file mode 100644
index 0000000..d590571
--- /dev/null
+++ b/scripts/ci-build-test-windows.sh
@@ -0,0 +1,156 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+YICES_SRC="$(cygpath -u "${YICES_SRC:?set YICES_SRC}")"
+YICES_PREFIX="${YICES_PREFIX:?set YICES_PREFIX}"
+JAVA_HOME_UNIX="$(cygpath -u "${JAVA_HOME:?set JAVA_HOME}")"
+JAVAC="${JAVA_HOME_UNIX}/bin/javac"
+JAVA="${JAVA_HOME_UNIX}/bin/java"
+JAR="${JAVA_HOME_UNIX}/bin/jar"
+
+win_path() {
+  cygpath -w "$1"
+}
+
+win_path_list() {
+  cygpath -wp "$1"
+}
+
+build_gmp() {
+  mkdir -p /tools/dynamic_gmp /tools/static_gmp
+  pushd /tools >/dev/null
+
+  local archive=gmp-6.3.0.tar.xz
+  if [[ ! -f "${archive}" ]]; then
+    curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+      https://ftp.gnu.org/gnu/gmp/${archive} -o "${archive}" || \
+    wget --tries=5 --timeout=20 -O "${archive}" https://ftp.gnu.org/gnu/gmp/${archive} || \
+    curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+      https://mirrors.kernel.org/gnu/gmp/${archive} -o "${archive}" || \
+    wget --tries=5 --timeout=20 -O "${archive}" https://mirrors.kernel.org/gnu/gmp/${archive} || \
+    curl -fL --retry 5 --retry-delay 2 --connect-timeout 20 --max-time 600 \
+      https://gmplib.org/download/gmp/${archive} -o "${archive}" || \
+    wget --tries=5 --timeout=20 -O "${archive}" https://gmplib.org/download/gmp/${archive}
+  fi
+
+  rm -rf gmp-6.3.0
+  tar xf "${archive}"
+  cd gmp-6.3.0
+  ./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx --enable-shared --disable-static --prefix=/tools/dynamic_gmp
+  make
+  make install
+  make clean
+  ./configure --host=x86_64-w64-mingw32 --build=i686-pc-cygwin --enable-cxx --enable-static --disable-shared --prefix=/tools/static_gmp
+  make
+  make install
+
+  popd >/dev/null
+}
+
+build_yices() {
+  pushd "${YICES_SRC}" >/dev/null
+  autoconf
+  ./configure \
+    --host=x86_64-w64-mingw32 \
+    --enable-thread-safety \
+    CPPFLAGS="-I/tools/dynamic_gmp/include" \
+    LDFLAGS="-L/tools/dynamic_gmp/lib" \
+    --with-static-gmp=/tools/static_gmp/lib/libgmp.a \
+    --with-static-gmp-include-dir=/tools/static_gmp/include
+  export LD_LIBRARY_PATH="/usr/local/lib/:${LD_LIBRARY_PATH:-}"
+  make OPTION=mingw64 MODE=release dist
+
+  local dist_dir
+  dist_dir="$(find build -type d -path '*/release/dist' | head -n 1)"
+  if [[ -z "${dist_dir}" ]]; then
+    echo "failed to locate Yices dist directory" >&2
+    exit 1
+  fi
+
+  rm -rf "${YICES_PREFIX}"
+  mkdir -p "${YICES_PREFIX}"
+  cp -R "${dist_dir}/." "${YICES_PREFIX}/"
+  popd >/dev/null
+}
+
+build_java_bindings() {
+  mkdir -p "${REPO_ROOT}/build/classes" "${REPO_ROOT}/build/test_classes" "${REPO_ROOT}/dist/lib"
+
+  pushd "${REPO_ROOT}" >/dev/null
+  find src/main/java/com/sri/yices -name '*.java' | sort > build/main-sources.txt
+  "${JAVAC}" \
+    -d "$(win_path "${REPO_ROOT}/build/classes")" \
+    -h "$(win_path "${REPO_ROOT}/src/main/java/com/sri/yices")" \
+    @"build/main-sources.txt"
+
+  x86_64-w64-mingw32-g++ \
+    -I "${JAVA_HOME_UNIX}/include" \
+    -I "${JAVA_HOME_UNIX}/include/win32" \
+    -I "${YICES_PREFIX}/include" \
+    -I /tools/dynamic_gmp/include \
+    -g -Wall -fpermissive \
+    -c src/main/java/com/sri/yices/yicesJNIforWindows.cpp \
+    -o build/yicesJNIforWindows.o
+
+  x86_64-w64-mingw32-g++ \
+    -shared \
+    -o dist/lib/yices2java.dll \
+    build/yicesJNIforWindows.o \
+    -L "${YICES_PREFIX}/lib" \
+    -L /tools/dynamic_gmp/lib \
+    -lyices -lgmp
+
+  "${JAR}" -cvfm \
+    "$(win_path "${REPO_ROOT}/dist/lib/yices.jar")" \
+    "$(win_path "${REPO_ROOT}/MANIFEST.txt")" \
+    -C "$(win_path "${REPO_ROOT}/build/classes")" .
+  popd >/dev/null
+}
+
+stage_runtime_dlls() {
+  cp "${YICES_PREFIX}/bin/libyices.dll" "${REPO_ROOT}/dist/lib/"
+  cp /tools/dynamic_gmp/bin/libgmp-10.dll "${REPO_ROOT}/dist/lib/"
+  cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libstdc++-6.dll "${REPO_ROOT}/dist/lib/"
+  cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libgcc_s_seh-1.dll "${REPO_ROOT}/dist/lib/"
+  cp /usr/x86_64-w64-mingw32/sys-root/mingw/bin/libwinpthread-1.dll "${REPO_ROOT}/dist/lib/"
+}
+
+run_tests() {
+  pushd "${REPO_ROOT}" >/dev/null
+  find src/test/java -name '*.java' | sort > build/test-sources.txt
+
+  local compile_cp
+  compile_cp="$(win_path_list "${REPO_ROOT}/dist/lib/yices.jar:${REPO_ROOT}/lib/junit-4.12.jar:${REPO_ROOT}/lib/hamcrest-core-1.3.jar")"
+  "${JAVAC}" \
+    -cp "${compile_cp}" \
+    -d "$(win_path "${REPO_ROOT}/build/test_classes")" \
+    @"build/test-sources.txt"
+
+  local runtime_cp runtime_path
+  runtime_cp="$(win_path_list "${REPO_ROOT}/build/test_classes:${REPO_ROOT}/dist/lib/yices.jar:${REPO_ROOT}/lib/junit-4.12.jar:${REPO_ROOT}/lib/hamcrest-core-1.3.jar")"
+  runtime_path="$(win_path_list "${REPO_ROOT}/dist/lib:/tools/dynamic_gmp/bin:/usr/x86_64-w64-mingw32/sys-root/mingw/bin")"
+
+  env PATH="${runtime_path}" \
+    "${JAVA}" \
+    "-Djava.library.path=$(win_path "${REPO_ROOT}/dist/lib")" \
+    -cp "${runtime_cp}" \
+    org.junit.runner.JUnitCore \
+    com.sri.yices.TestBigRationals \
+    com.sri.yices.TestConstructor \
+    com.sri.yices.TestContext \
+    com.sri.yices.TestStatus \
+    com.sri.yices.TestTypes \
+    com.sri.yices.TestYices \
+    com.sri.yices.TestModels \
+    com.sri.yices.TestTermComponents \
+    com.sri.yices.TestThreads
+  popd >/dev/null
+}
+
+build_gmp
+build_yices
+build_java_bindings
+stage_runtime_dlls
+run_tests
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/Makefile b/src/main/java/com/sri/yices/Makefile
index 158571b..88eaff0 100644
--- a/src/main/java/com/sri/yices/Makefile
+++ b/src/main/java/com/sri/yices/Makefile
@@ -56,9 +56,15 @@ libyices2java_install_name := $(YICES_JNI)/libyices2java.dylib
 # we ignore versions and soname for now
 
 # default include directories for jni.h and jni_md.h
-CPPFLAGS := -I $(JAVA_HOME)/include -I $(JAVA_HOME)/include/$(OS)
-CXXFLAGS := -g -fPIC
-LIBS := -lyices -lgmp
+GMP_CPPFLAGS ?= $(shell pkg-config --cflags gmp 2>/dev/null)
+GMP_LIBS ?= $(shell pkg-config --libs gmp 2>/dev/null)
+
+CPPFLAGS += -I $(JAVA_HOME)/include -I $(JAVA_HOME)/include/$(OS) $(GMP_CPPFLAGS)
+CXXFLAGS += -g -fPIC
+ifeq ($(strip $(GMP_LIBS)),)
+GMP_LIBS := -lgmp
+endif
+LIBS += -lyices $(GMP_LIBS)
 
 CXX ?= g++
 
@@ -77,16 +83,16 @@ $(YICES_CLASSPATH)/com/sri/yices/%.class: %.java
 	$(JAVAC) -d $(YICES_CLASSPATH) *.java
 
 com_sri_yices_Yices.h: $(YICES_CLASSPATH)/com/sri/yices/Yices.class
-	$(JAVAC) -h . *.java
+	$(JAVAC) -d $(YICES_CLASSPATH) -h . *.java
 
 yicesJNI.o: yicesJNI.cpp com_sri_yices_Yices.h
 	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -Wall -c yicesJNI.cpp
 
 libyices2java.dylib: yicesJNI.o
-	$(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
+	$(CXX) $(CPPFLAGS) $(CXXFLAGS) $(LDFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
 
 libyices2java.so: yicesJNI.o
-	$(CXX) $(CFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)
+	$(CXX) $(CPPFLAGS) $(CXXFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)
 
 LIBDIR := $(YICES_JNI)
 
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,
diff --git a/src/main/java/com/sri/yices/yicesJNI.cpp b/src/main/java/com/sri/yices/yicesJNI.cpp
index 27290e2..abb7c96 100644
--- a/src/main/java/com/sri/yices/yicesJNI.cpp
+++ b/src/main/java/com/sri/yices/yicesJNI.cpp
@@ -2674,7 +2674,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);
       }
     }
@@ -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<param_t*>(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<jlong>(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<jlong>(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<jlong>(model);
       env->SetLongArrayRegion(marr, 0, 1, &mdl);
     }
diff --git a/src/test/java/com/sri/yices/TestTermComponents.java b/src/test/java/com/sri/yices/TestTermComponents.java
new file mode 100644
index 0000000..7329fba
--- /dev/null
+++ b/src/test/java/com/sri/yices/TestTermComponents.java
@@ -0,0 +1,132 @@
+package com.sri.yices;
+
+import org.junit.Assert;
+import org.junit.Test;
+
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+import java.math.BigInteger;
+import java.util.HashMap;
+import java.util.Map;
+
+import static org.junit.Assume.assumeTrue;
+
+public class TestTermComponents {
+    @Test
+    public void testProjectedComponentsWhenAvailable() throws Exception {
+        assumeTrue(TestAssumptions.IS_YICES_INSTALLED);
+
+        Method sumComponent = optionalMethod("sumComponent");
+        Method productComponent = optionalMethod("productComponent");
+        if (sumComponent == null || productComponent == null) {
+            return;
+        }
+
+        int x = Terms.newUninterpretedTerm("term_components_x", Types.INT);
+        int y = Terms.newUninterpretedTerm("term_components_y", Types.INT);
+        int bvType = Types.bvType(8);
+        int bx = Terms.newUninterpretedTerm("term_components_bx", bvType);
+        int by = Terms.newUninterpretedTerm("term_components_by", bvType);
+
+        try {
+            int arith = Terms.rationalPoly(new long[] { 3, -5 }, new long[] { 2, 1 }, new int[] { x, y });
+            Assert.assertTrue(Terms.isSum(arith));
+
+            Map<Integer, BigRational> arithComponents = collectSumComponents(sumComponent, arith);
+            Assert.assertEquals(2, arithComponents.size());
+            Assert.assertEquals(new BigRational(BigInteger.valueOf(3), BigInteger.valueOf(2)), arithComponents.get(x));
+            Assert.assertEquals(new BigRational(BigInteger.valueOf(-5), BigInteger.ONE), arithComponents.get(y));
+
+            int bsum = Terms.bvAdd(
+                    Terms.bvMul(Terms.bvConst(8, 3), bx),
+                    Terms.bvMul(Terms.bvConst(8, 5), by));
+            Assert.assertTrue(Terms.isBvSum(bsum));
+
+            Map<Integer, boolean[]> bvComponents = collectBvSumComponents(sumComponent, bsum);
+            Assert.assertEquals(2, bvComponents.size());
+            Assert.assertArrayEquals(Terms.bvConstValue(Terms.bvConst(8, 3)), bvComponents.get(bx));
+            Assert.assertArrayEquals(Terms.bvConstValue(Terms.bvConst(8, 5)), bvComponents.get(by));
+
+            int product = Terms.mul(Terms.power(x, 3), Terms.power(y, 2));
+            Assert.assertTrue(Terms.isProduct(product));
+
+            Map<Integer, Integer> productComponents = collectProductComponents(productComponent, product);
+            Assert.assertEquals(2, productComponents.size());
+            Assert.assertEquals(Integer.valueOf(3), productComponents.get(x));
+            Assert.assertEquals(Integer.valueOf(2), productComponents.get(y));
+        } finally {
+            Terms.removeName("term_components_x");
+            Terms.removeName("term_components_y");
+            Terms.removeName("term_components_bx");
+            Terms.removeName("term_components_by");
+        }
+    }
+
+    private static Method optionalMethod(String name) {
+        try {
+            return Yices.class.getMethod(name, int.class, int.class);
+        } catch (NoSuchMethodException e) {
+            return null;
+        }
+    }
+
+    private static Map<Integer, BigRational> collectSumComponents(Method method, int term) throws Exception {
+        Map<Integer, BigRational> result = new HashMap<>();
+        for (int idx = 0; ; idx++) {
+            Object component = invoke(method, term, idx);
+            if (component == null) {
+                break;
+            }
+            int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+            Object factor = component.getClass().getMethod("getFactor").invoke(component);
+            Assert.assertTrue(factor instanceof BigRational);
+            result.put(child, (BigRational) factor);
+        }
+        return result;
+    }
+
+    private static Map<Integer, boolean[]> collectBvSumComponents(Method method, int term) throws Exception {
+        Map<Integer, boolean[]> result = new HashMap<>();
+        for (int idx = 0; ; idx++) {
+            Object component = invoke(method, term, idx);
+            if (component == null) {
+                break;
+            }
+            int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+            Object factor = component.getClass().getMethod("getFactor").invoke(component);
+            if (factor instanceof boolean[]) {
+                result.put(child, (boolean[]) factor);
+            }
+        }
+        return result;
+    }
+
+    private static Map<Integer, Integer> collectProductComponents(Method method, int term) throws Exception {
+        Map<Integer, Integer> result = new HashMap<>();
+        for (int idx = 0; ; idx++) {
+            Object component = invoke(method, term, idx);
+            if (component == null) {
+                break;
+            }
+            int child = (Integer) component.getClass().getMethod("getTerm").invoke(component);
+            int power = (Integer) component.getClass().getMethod("getPower").invoke(component);
+            result.put(child, power);
+        }
+        return result;
+    }
+
+    private static Object invoke(Method method, int term, int idx) throws Exception {
+        try {
+            return method.invoke(null, term, idx);
+        } catch (InvocationTargetException e) {
+            Throwable cause = e.getCause();
+            if (cause instanceof Error) {
+                throw (Error) cause;
+            }
+            if (cause instanceof Exception) {
+                throw (Exception) cause;
+            }
+            throw e;
+        }
+    }
+}