diffblue · kroening · Jul 12, 2026 · Jul 12, 2026
@@ -1,4 +1,3 @@
-jbmc/src/miniz/miniz.cpp
-jbmc/src/miniz/miniz.h
+3p/
 src/cprover/wcwidth.c
 unit/catch/catch.hpp
@@ -45,7 +45,6 @@ jobs:
             ccache -p
             echo "Build with gmake"
             # don't do JBMC as to keep the overall time in check
-            gmake -C src minisat2-download
             gmake -C src -j2 CXX="ccache clang++"
             # gmake -C jbmc/src setup-submodules
             # gmake -C jbmc/src -j2 CXX="ccache clang++"
@@ -116,7 +115,6 @@ jobs:
             ccache -p
             echo "Build with gmake"
             # don't do JBMC so as to keep the overall time in check
-            gmake -C src minisat2-download
             gmake -C src -j2 CXX="ccache clang++"
             # gmake -C jbmc/src setup-submodules
             # gmake -C jbmc/src -j2 CXX="ccache clang++"
@@ -185,7 +183,6 @@ jobs:
             ccache -p
             echo "Build with gmake"
             # don't do JBMC so as to keep the overall time in check
-            gmake -C src minisat2-download
             gmake -C src -j2 CXX="ccache g++"
             # gmake -C jbmc/src setup-submodules
             # gmake -C jbmc/src -j2 CXX="ccache g++"

@@ -41,7 +41,6 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build CBMC tools
         run: |
-          make -C src minisat2-download
           make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j4
       - name: Print ccache stats
         run: ccache -s

@@ -40,7 +40,6 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build CBMC tools
         run: |
-          make -C src minisat2-download
           make -C src CXX='ccache /usr/bin/clang++' cbmc.dir goto-cc.dir goto-diff.dir -j4
       - name: Print ccache stats
         run: ccache -s

@@ -44,7 +44,6 @@ jobs:
 
     - name: Build
       run: |
-        make -C src minisat2-download
         make -C src       -j4
         make -C unit      -j4
         make -C jbmc/src  -j4

@@ -21,7 +21,6 @@ jobs:
           sudo apt-get update
           sudo apt-get install --no-install-recommends -y build-essential flex bison maven ccache clang-19 clang++-19
           sudo apt-get install --no-install-recommends -y csmith libcsmith-dev
-          make -C src minisat2-download
       - name: Restore ccache
         id: restore-ccache
         uses: actions/cache/restore@v6

@@ -115,7 +115,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download cadical-download
+          make -C src cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -140,7 +140,7 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build with make
         run: |
-          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../3p/minisat-2.2.1-patched CADICAL=../../cadical
           make -C unit      -j${{env.linux-vcpus}}
           make -C jbmc/src  -j${{env.linux-vcpus}}
           make -C jbmc/unit -j${{env.linux-vcpus}}
@@ -191,7 +191,6 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -319,7 +318,7 @@ jobs:
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
-          make -C src minisat2-download cadical-download
+          make -C src cadical-download
           cpanm Thread::Pool::Simple
       - name: Confirm z3 solver is available and log the version installed
         run: z3 --version
@@ -348,7 +347,7 @@ jobs:
           make -C src/cpp library_check
       - name: Build with make
         run: |
-          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C src       -j${{env.linux-vcpus}} MINISAT2=../../3p/minisat-2.2.1-patched CADICAL=../../cadical
           make -C unit      -j${{env.linux-vcpus}}
           make -C jbmc/src  -j${{env.linux-vcpus}}
           make -C jbmc/unit -j${{env.linux-vcpus}}
@@ -734,8 +733,8 @@ jobs:
         run: ccache -z --max-size=500M
       - name: Build using Make
         run: |
-          make -C src minisat2-download cadical-download
-          make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C src cadical-download
+          make -C src -j4 CXX="ccache clang++" MINISAT2=../../3p/minisat-2.2.1-patched CADICAL=../../cadical
           make -C jbmc/src -j4 CXX="ccache clang++"
           make -C unit "CXX=ccache clang++"
           make -C jbmc/unit "CXX=ccache clang++"
@@ -1008,8 +1007,6 @@ jobs:
         run: |
           clcache -z
           clcache -M 2147483648
-      - name: Download minisat with make
-        run: make -C src minisat2-download
       - name: Build CBMC with make
         run: |
           make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
@@ -1206,7 +1203,7 @@ jobs:
       - name: Run include-what-you-use
         run: |
           iwyu_tool -p build/compile_commands.json -j${{env.linux-vcpus}} | tee includes.txt
-          if sed '/minisat2-src/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
+          if sed '/minisat-2.2.1-patched/,/^--$/d' includes.txt | grep '^- ' -B1 ; then
             echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
             exit 1
           fi
@@ -82,7 +82,6 @@ unit/gdb.txt
 *~
 
 # libs downloaded by make [name]-download
-minisat*/
 cadical*/
 glucose-syrup/
 

@@ -0,0 +1,50 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: minisat2
+Upstream-Contact: Niklas Sorensson <niklasso@gmail.com>
+Source: http://minisat.se/
+Comment: MiniSat is a minimalistic, high-performance SAT solver. It is used
+ by src/solvers/sat/satcheck_minisat2.{cpp,h}, and is the default SAT back-end
+ of CBMC.
+ .
+ The directory minisat-2.2.1-original/ is byte-for-byte identical to the
+ contents of the Debian source tarball
+ http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
+ (MD5 27faa19ee0508660bd6fb7f894646d42), which is version 2.2.1 of MiniSat
+ as released by Debian; upstream itself never tagged a 2.2.1 release.
+ .
+ The directory minisat-2.2.1-patched/ is the copy that is actually built. It
+ differs from minisat-2.2.1-original/ by the patch that was previously kept
+ in scripts/minisat-2.2.1-patch:
+  * fixes for compiler warnings and errors with newer C++ compilers and
+    with Visual Studio (parenthesization, template friend declarations,
+    dangling else, zero-length arrays, PRIi64 format macros);
+  * the zlib-based DIMACS parser in ParseUtils.h is disabled;
+  * fpu_control.h is only included with glibc;
+  * out-of-memory conditions are reported by exception rather than
+    depending on errno.
+ The patch can be re-created by diffing the two directories.
+
+Files: minisat-2.2.1-original/* minisat-2.2.1-patched/*
+Copyright: 2003-2006, Niklas Een, Niklas Sorensson
+           2007-2010, Niklas Sorensson
+License: Expat
+
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a
+ copy of this software and associated documentation files (the
+ "Software"), to deal in the Software without restriction, including
+ without limitation the rights to use, copy, modify, merge, publish,
+ distribute, sublicense, and/or sell copies of the Software, and to
+ permit persons to whom the Software is furnished to do so, subject to
+ the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included
+ in all copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+ OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+ LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+ OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
@@ -0,0 +1,47 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: miniz
+Upstream-Contact: Rich Geldreich <richgel99@gmail.com>
+Source: https://github.com/richgel999/miniz
+Comment: miniz is a lossless, high performance data compression library that
+ implements the zlib (RFC 1950) and Deflate (RFC 1951) compressed data format
+ specification standards, with ZIP archive reading support. The vendored copy
+ consists of the amalgamated files miniz.h and miniz.cpp (upstream: miniz.c),
+ and is used by jbmc/src/java_bytecode/ to read .jar files.
+ .
+ The in-tree files are based on upstream commit
+ 0c30a001bc3c70770a8742ff00899e662f040c75 (release 3.0.2 plus all upstream
+ changes up to and including the fix for CVE-2018-12913), with the
+ following local modifications:
+  * miniz.c has been renamed to miniz.cpp and is compiled as C++;
+  * the configuration macros MINIZ_NO_TIME, MINIZ_NO_DEFLATE_APIS,
+    MINIZ_NO_ARCHIVE_WRITING_APIS, MINIZ_NO_ZLIB_APIS and
+    MINIZ_NO_ZLIB_COMPATIBLE_NAMES are enabled in miniz.h;
+  * compiler warnings (conversion and unhandled-enum warnings, in
+    particular with Visual Studio) have been silenced;
+  * functions that are only used when archive writing is enabled have
+    been removed.
+
+Files: miniz-3.0.2/*
+Copyright: 2013-2014, RAD Game Tools and Valve Software
+           2010-2014, Rich Geldreich and Tenacious Software LLC
+           2016, Martin Raiber
+License: Expat
+
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a copy
+ of this software and associated documentation files (the "Software"), to
+ deal in the Software without restriction, including without limitation the
+ rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+ sell copies of the Software, and to permit persons to whom the Software is
+ furnished to do so, subject to the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included in
+ all copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+ FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+ IN THE SOFTWARE.
@@ -0,0 +1,7 @@
+*.d
+*.o
+minisat
+minisat_core
+config.mk
+lib*.a
+lib*.so*
@@ -0,0 +1,21 @@
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.