diff --git a/.cirrus.yml b/.cirrus.yml
index f1244a2410..6de1dc52cf 100644
--- a/.cirrus.yml
+++ b/.cirrus.yml
@@ -1,8 +1,7 @@
 task:
   freebsd_instance:
     matrix:
-      - image_family: freebsd-13-2-snap
-      - image_family: freebsd-14-0-snap
+      - image_family: freebsd-15-0-snap
   deps_script:
     - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf
     - env ASSUME_ALWAYS_YES=yes pkg update -f
@@ -10,7 +9,7 @@ task:
   build_script:
     - mkdir build
     - cd build
-    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 ..
+    - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON -DENABLE_WARNINGS_AS_ERRORS=1 -DENABLE_FP_RUNTIME=1 ..
     - gmake
   test_script:
     - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg
diff --git a/.github/workflows/build-in-base-env.yml b/.github/workflows/build-in-base-env.yml
deleted file mode 100644
index daf22bff94..0000000000
--- a/.github/workflows/build-in-base-env.yml
+++ /dev/null
@@ -1,25 +0,0 @@
-name: Build in UTBot base_env
-
-on:
-  pull_request:
-    branches: [utbot-main]
-  push:
-    branches: [utbot-main]
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-    container:
-      image: ghcr.io/unittestbot/utbotcpp/base_env:02-02-2022
-      credentials:
-        username: ${{ github.actor }}
-        password: ${{ secrets.GITHUB_TOKEN }}
-    steps:
-      - name: Checkout repository
-        uses: actions/checkout@v2
-      - name: Run build.sh
-        run: |
-          ./build.sh
-      - name: Run tests
-        run: |
-          cd build && ninja check
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
index 376929fb22..433923b8b5 100644
--- a/.github/workflows/build.yaml
+++ b/.github/workflows/build.yaml
@@ -24,7 +24,8 @@ env:
   ENABLE_OPTIMIZED: 1
   ENABLE_DEBUG: 1
   ENABLE_WARNINGS_AS_ERRORS: ${{ github.event_name == 'workflow_dispatch' && inputs.warnings_as_errors || 1}}
-  GTEST_VERSION: 1.11.0
+  ENABLE_FP_RUNTIME: 1
+  GTEST_VERSION: 1.16.0
   KLEE_RUNTIME_BUILD: "Debug+Asserts"
   LLVM_VERSION: 11
   MINISAT_VERSION: "master"
@@ -43,7 +44,7 @@ env:
 
 jobs:
   Linux:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-22.04
     strategy:
       matrix:
         name: [
@@ -160,7 +161,9 @@ jobs:
     env:
       LLVM_VERSION: 14
       BASE: /tmp
-      SOLVERS: STP
+      SOLVERS: Z3
+      Z3_VERSION: 4.14.1
+      ENABLE_FP_RUNTIME: 0
       UCLIBC_VERSION: 0
       USE_TCMALLOC: 0
       USE_LIBCXX: 0
diff --git a/.github/workflows/docker_release_push.yml b/.github/workflows/docker_release_push.yml
index 7337e3d436..31d05363c9 100644
--- a/.github/workflows/docker_release_push.yml
+++ b/.github/workflows/docker_release_push.yml
@@ -6,23 +6,24 @@ on:
 
 jobs:
   push_to_registry:
-    name: Push Docker Image to Docker Hub
+    name: Push Docker Image to Github Registry
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
         uses: actions/checkout@v3
 
-      - name: Log in to Docker Hub
+      - name: Log in to Github Registry
         uses: docker/login-action@f4ef78c080cd8ba55a85445d5b36e214a81df20a
         with:
-          username: ${{ secrets.DOCKER_USERNAME }}
-          password: ${{ secrets.DOCKER_PASSWORD }}
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GH_REGISTRY }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
         uses: docker/metadata-action@9ec57ed1fcdbf14dcef7dfbe97b2010124a938b7
         with:
-          images: klee/klee
+          images: ghcr.io/unittestbot/klee/klee
 
       - name: Build and push Docker image
         uses: docker/build-push-action@3b5e8027fcad23fda98b2e3ac259d8d67585f671
@@ -31,4 +32,4 @@ jobs:
           file: ./Dockerfile
           push: true
           tags: ${{ steps.meta.outputs.tags }}
-          labels: ${{ steps.meta.outputs.labels }}
\ No newline at end of file
+          labels: ${{ steps.meta.outputs.labels }}
diff --git a/Dockerfile b/Dockerfile
index 7055a9d77b..2ef2629fd5 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,33 +1,40 @@
-FROM ghcr.io/klee/llvm:130_O_D_A_ubuntu_jammy-20230126 as llvm_base
-FROM ghcr.io/klee/gtest:1.11.0_ubuntu_jammy-20230126 as gtest_base
-FROM ghcr.io/klee/uclibc:klee_uclibc_v1.3_130_ubuntu_jammy-20230126 as uclibc_base
-FROM ghcr.io/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 as tcmalloc_base
-FROM ghcr.io/klee/stp:2.3.3_ubuntu_jammy-20230126 as stp_base
-FROM ghcr.io/klee/z3:4.8.15_ubuntu_jammy-20230126 as z3_base
-FROM ghcr.io/klee/libcxx:130_ubuntu_jammy-20230126 as libcxx_base
-FROM ghcr.io/klee/sqlite:3400100_ubuntu_jammy-20230126 as sqlite3_base
-FROM llvm_base as intermediate
+FROM ghcr.io/unittestbot/klee/llvm:140_O_D_A_ubuntu_jammy-20230126 AS llvm_base
+FROM ghcr.io/unittestbot/klee/gtest:1.16.0_ubuntu_jammy-20230126 AS gtest_base
+FROM ghcr.io/unittestbot/klee/uclibc:klee_uclibc_v1.4_140_ubuntu_jammy-20230126 AS uclibc_base
+FROM ghcr.io/unittestbot/klee/tcmalloc:2.9.1_ubuntu_jammy-20230126 AS tcmalloc_base
+FROM ghcr.io/unittestbot/klee/stp:2.3.3_ubuntu_jammy-20230126 AS stp_base
+FROM ghcr.io/unittestbot/klee/z3:4.8.15_ubuntu_jammy-20230126 AS z3_base
+FROM ghcr.io/unittestbot/klee/bitwuzla:0.7.0_ubuntu_jammy-20230126 AS bitwuzla_base
+FROM ghcr.io/unittestbot/klee/libcxx:140_ubuntu_jammy-20230126 AS libcxx_base
+FROM ghcr.io/unittestbot/klee/sqlite:3400100_ubuntu_jammy-20230126 AS sqlite3_base
+FROM ghcr.io/unittestbot/klee/immer:v0.8.1_ubuntu_jammy-20230126 AS immer_base
+FROM ghcr.io/unittestbot/klee/json:v3.11.3_ubuntu_jammy-20230126 AS json_base
+FROM llvm_base AS intermediate
 COPY --from=gtest_base /tmp /tmp/
 COPY --from=uclibc_base /tmp /tmp/
 COPY --from=tcmalloc_base /tmp /tmp/
 COPY --from=stp_base /tmp /tmp/
 COPY --from=z3_base /tmp /tmp/
+COPY --from=bitwuzla_base /tmp /tmp/
 COPY --from=libcxx_base /tmp /tmp/
 COPY --from=sqlite3_base /tmp /tmp/
+COPY --from=immer_base /tmp /tmp/
+COPY --from=json_base /tmp /tmp/
 ENV COVERAGE=0
 ENV USE_TCMALLOC=1
 ENV BASE=/tmp
 ENV BUILD_SUFFIX="default"
-ENV LLVM_VERSION=13.0
+ENV LLVM_VERSION=14
 ENV ENABLE_DOXYGEN=1
 ENV ENABLE_OPTIMIZED=1
 ENV ENABLE_DEBUG=1
 ENV DISABLE_ASSERTIONS=0
 ENV ENABLE_WARNINGS_AS_ERRORS=1
+ENV ENABLE_FP_RUNTIME=1
 ENV REQUIRES_RTTI=0
-ENV SOLVERS=STP:Z3
-ENV GTEST_VERSION=1.11.0
-ENV UCLIBC_VERSION=klee_uclibc_v1.3
+ENV SOLVERS=BITWUZLA:Z3:STP
+ENV GTEST_VERSION=1.16.0
+ENV UCLIBC_VERSION=klee_uclibc_v1.4
 ENV TCMALLOC_VERSION=2.9.1
 ENV SANITIZER_BUILD=
 ENV STP_VERSION=2.3.3
@@ -37,8 +44,9 @@ ENV USE_LIBCXX=1
 ENV KLEE_RUNTIME_BUILD="Debug+Asserts"
 ENV SQLITE_VERSION=3400100
 ENV JSON_VERSION=v3.11.3
+ENV BITWUZLA_VERSION=0.7.0
 ENV IMMER_VERSION=v0.8.1
-LABEL maintainer="KLEE Developers"
+LABEL maintainer="KLEEF Developers"
 
 # TODO remove adding sudo package
 # Create ``klee`` user for container with password ``klee``.
@@ -60,7 +68,7 @@ RUN /tmp/klee_src/scripts/build/build.sh --debug --install-system-deps klee && p
     sudo rm -rf /var/lib/apt/lists/*
 
 
-ENV PATH="$PATH:/tmp/llvm-130-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
+ENV PATH="$PATH:/tmp/llvm-140-install_O_D_A/bin:/home/klee/klee_build/bin:/home/klee/.local/bin"
 ENV BASE=/tmp
 # Add path to local LLVM installation - let system install precede local install
 RUN /bin/bash -c 'echo "export \"PATH=$PATH:$(cd ${BASE}/llvm-*-install*/bin/ && pwd)\" >> /home/klee/.bashrc"'
diff --git a/build.sh b/build.sh
index 33cf59ce8c..0c79bb5a2d 100755
--- a/build.sh
+++ b/build.sh
@@ -20,6 +20,7 @@ KLEE_RUNTIME_BUILD="Release"
 COVERAGE=0
 ENABLE_DOXYGEN=0
 USE_TCMALLOC=0
+ENABLE_FP_RUNTIME=1
 TCMALLOC_VERSION=2.9.1
 USE_LIBCXX=1
 # Also required despite not being mentioned in the guide
@@ -71,4 +72,4 @@ else
 fi
 done
 
-BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ./scripts/build/build.sh klee --install-system-deps
+BASE="$BASE" BUILD_SUFFIX="$BUILD_SUFFIX" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC TCMALLOC_VERSION=$TCMALLOC_VERSION USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION IMMER_VERSION=$IMMER_VERSION SANITIZER_BUILD=$SANITIZER_BUILD SANITIZER_LLVM_VERSION=$SANITIZER_LLVM_VERSION ENABLE_WARNINGS_AS_ERRORS=$ENABLE_WARNINGS_AS_ERRORS ENABLE_FP_RUNTIME=$ENABLE_FP_RUNTIME ./scripts/build/build.sh klee --install-system-deps
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b06d2fee5b..79f7e7ce6f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2528,8 +2528,9 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       uint64_t size = 0; // total size of variadic arguments
       bool requires16ByteAlignment = false;
 
-      uint64_t offsets[callingArgs]; // offsets of variadic arguments
-      uint64_t argWidth;             // width of current variadic argument
+      std::vector<uint64_t> offsets;
+      offsets.reserve(callingArgs); // offsets of variadic arguments
+      uint64_t argWidth;            // width of current variadic argument
 
       const CallBase &cb = cast<CallBase>(*i);
       for (unsigned k = funcArgs; k < callingArgs; k++) {
diff --git a/scripts/build/p-gtest.inc b/scripts/build/p-gtest.inc
index d4a2d498d5..da274a2f86 100644
--- a/scripts/build/p-gtest.inc
+++ b/scripts/build/p-gtest.inc
@@ -1,14 +1,13 @@
 setup_build_variables_gtest() {
-  GTEST_INSTALL_PATH="${BASE}/googletest-release-${GTEST_VERSION}"
+  GTEST_INSTALL_PATH="${BASE}/googletest-${GTEST_VERSION}"
   return 0
 }
 
 download_gtest() {
   cd "${BASE}" || exit 1
-  wget "https://github.com/google/googletest/archive/release-${GTEST_VERSION}.zip"
-  unzip -o "release-${GTEST_VERSION}.zip"
-  rm "release-${GTEST_VERSION}.zip"
-  touch "${GTEST_INSTALL_PATH}"/.is_installed
+  wget "https://github.com/google/googletest/archive/refs/tags/v${GTEST_VERSION}.zip"
+  unzip -o "v${GTEST_VERSION}.zip"
+  rm "v${GTEST_VERSION}.zip"
 }
 
 build_gtest() {
@@ -42,4 +41,4 @@ get_docker_config_id_gtest() {
     setup_build_variables_gtest
     echo "${GTEST_VERSION}"
   )
-}
\ No newline at end of file
+}
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc
index 89d1b5f0df..5be1cd292e 100644
--- a/scripts/build/p-klee.inc
+++ b/scripts/build/p-klee.inc
@@ -91,12 +91,11 @@ fi
       echo "Z3"
       KLEE_Z3_CONFIGURE_OPTION=(
         "-DENABLE_SOLVER_Z3=TRUE"
-        "-DZ3_INCLUDE_DIRS=${Z3_INSTALL_PATH}/include"
-        "-DZ3_LIBRARIES=${Z3_INSTALL_PATH}/lib/libz3.so"
       )
+      CMAKE_PREFIX_PATH+=("${Z3_INSTALL_PATH}")
       KLEE_FLOATING_POINT=(
-        "-DENABLE_FLOATING_POINT=TRUE"
-        "-DENABLE_FP_RUNTIME=TRUE"
+        "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
+        "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
       )
       ;;
     metasmt)
@@ -114,11 +113,10 @@ fi
       KLEE_BITWUZLA_CONFIGURE_OPTION=(
         "-DENABLE_SOLVER_BITWUZLA=TRUE"
       )
-      
       CMAKE_PREFIX_PATH+=("${BITWUZLA_INSTALL_PATH}")
       KLEE_FLOATING_POINT=(
-        "-DENABLE_FLOATING_POINT=TRUE"
-        "-DENABLE_FP_RUNTIME=TRUE"
+        "-DENABLE_FLOATING_POINT=${ENABLE_FP_RUNTIME}"
+        "-DENABLE_FP_RUNTIME=${ENABLE_FP_RUNTIME}"
       )
       echo "bitwuzla"
       ;;
diff --git a/scripts/build/p-z3-osx.inc b/scripts/build/p-z3-osx.inc
index bce11aabad..5abaadcb5d 100644
--- a/scripts/build/p-z3-osx.inc
+++ b/scripts/build/p-z3-osx.inc
@@ -1,13 +1,14 @@
-install_binary_artifact_z3 () {
-  set +e
-  brew install python@2
-  if [[ "X$?" != "X0" ]]; then
-     brew link --overwrite python@2
-  fi
-  set -e
+#!/usr/bin/env bash
+# shellcheck disable=SC2034
+
+install_binary_artifact_z3() {
   brew install z3
 }
 
-is_installed_z3() {
-    [[ -f "/usr/local/opt/z3/bin/z3" ]]
-}
\ No newline at end of file
+setup_artifact_variables_z3() {
+  Z3_INSTALL_PATH="$(brew --cellar z3)/${Z3_VERSION}"
+}
+
+install_build_dependencies_z3() {
+  return 0
+}
diff --git a/scripts/build/v-klee.inc b/scripts/build/v-klee.inc
index 4a1107e18e..b653419f1b 100644
--- a/scripts/build/v-klee.inc
+++ b/scripts/build/v-klee.inc
@@ -7,6 +7,7 @@ required_variables_klee=(
   "USE_LIBCXX"
   "ENABLE_DOXYGEN"
   "ENABLE_WARNINGS_AS_ERRORS"
+  "ENABLE_FP_RUNTIME"
 )
 
 required_variables_check_klee() {
@@ -15,6 +16,7 @@ required_variables_check_klee() {
   check_bool "USE_LIBCXX"
   check_bool "ENABLE_DOXYGEN"
   check_bool "ENABLE_WARNINGS_AS_ERRORS"
+  check_bool "ENABLE_FP_RUNTIME"
 }
 
 # On which artifacts does KLEE depend on
diff --git a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c
index dfb550f73e..7596f62d60 100644
--- a/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c
+++ b/test/Industry/CoverageErrorCall/egcd3-ll_unwindbound10.c
@@ -78,6 +78,7 @@ int main() {
 // REQUIRES: bitwuzla
 // REQUIRES: not-asan
 // REQUIRES: not-msan
+// REQUIRES: not-ubsan
 // REQUIRES: not-darwin
 // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=60 --32 --debug --write-ktests %s 2>&1 | FileCheck %s
 // CHECK: KLEE: WARNING: 100.00% Reachable Reachable
diff --git a/test/Solver/sina2f.c b/test/Solver/sina2f.c
index c732bf2ddb..93e3ecbb69 100644
--- a/test/Solver/sina2f.c
+++ b/test/Solver/sina2f.c
@@ -1,6 +1,7 @@
 // REQUIRES: bitwuzla
 // REQUIRES: not-asan
 // REQUIRES: not-msan
+// REQUIRES: not-ubsan
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s