<pre style='margin:0'>
Ryan Schmidt (ryandesign) pushed a commit to branch master
in repository macports-ports.

</pre>
<p><a href="https://github.com/macports/macports-ports/commit/0698ac75033eef17e501c667b2b385c7ec34f9ff">https://github.com/macports/macports-ports/commit/0698ac75033eef17e501c667b2b385c7ec34f9ff</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 0698ac75033eef17e501c667b2b385c7ec34f9ff
</span>Author: Ryan Schmidt <ryandesign@macports.org>
AuthorDate: Thu Jan 6 10:31:35 2022 -0600

<span style='display:block; white-space:pre;color:#404040;'>    boolector: Update to 3.2.2
</span><span style='display:block; white-space:pre;color:#404040;'>    
</span><span style='display:block; white-space:pre;color:#404040;'>    Closes: https://trac.macports.org/ticket/38631
</span>---
 math/boolector/Portfile                      |  70 +++++++-------
 math/boolector/files/DYLD_LIBRARY_PATH.patch | 134 +++++++++++++++++++++++++++
 math/boolector/files/btor2tools.patch        |  39 ++++++++
 math/boolector/files/googletest.patch        |  43 +++++++++
 math/boolector/files/patch-btorexp.c.diff    |  11 ---
 math/boolector/files/patch-btorsat.c.diff    |  15 ---
 math/boolector/files/patch-configure.diff    |  25 -----
 math/boolector/files/patch-makefile.in.diff  |  11 ---
 8 files changed, 254 insertions(+), 94 deletions(-)

<span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/Portfile b/math/boolector/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index c25880ee68b..76640a17067 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/boolector/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/boolector/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,53 +1,59 @@
</span> # -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4
 
 PortSystem 1.0
<span style='display:block; white-space:pre;background:#e0ffe0;'>+PortGroup           cmake 1.1
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+PortGroup           github 1.0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+github.setup        Boolector boolector 3.2.2
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+revision            0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+checksums           rmd160  2179695681ba6abbb2812a06caf8a252accc7bc5 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    sha256  9a5bdbacf83f2dd81dbed1e1a9f923766807470afa29b73729c947ae769d42b9 \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    size    1566009
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-name                boolector
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-version             1.4.1-376e6b0-110304
</span> categories          math science
<span style='display:block; white-space:pre;background:#ffe0e0;'>-platforms           darwin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-license             GPL-3
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+license             MIT
</span> maintainers         nomaintainer
<span style='display:block; white-space:pre;background:#ffe0e0;'>-description         Boolector is an SMT solver for the theory of bit-vectors
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+description         an SMT solver for the theory of bit-vectors
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span> long_description    \
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    Boolector is an SMT solver for the theory of bit-vectors and the \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    Boolector is {*}${description} and the \
</span>     extensional theory of arrays over bit-vectors. It won first places in the \
     prestigious bit-vector and bit-vector with arrays tracks in the SMT \
     competition 2008. In the latest SMT competition, it won the second place \
     in the bit-vector division and again the first place in the division of \
     bit-vectors and arrays.
 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-homepage            http://fmv.jku.at/boolector/
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-master_sites        ${homepage}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+github.tarball_from archive
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-checksums           rmd160  0611fdd7edf840bc0d7e37d49b2394102465c71f \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    sha256  5987e056eba62895aba89f9e6e921ab757d219787282e0ecac7295665fafa72b
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# To run tests, but configure fails without it.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_build-append \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    port:gtest
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-depends_lib         port:picosat
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+# Static library.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_build-append \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    port:picosat
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-installs_libs       no
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+depends_lib-append  port:btor2tools \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    port:gmp
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-patchfiles          patch-configure.diff \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    patch-btorexp.c.diff \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    patch-btorsat.c.diff \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-                    patch-makefile.in.diff
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+patchfiles          DYLD_LIBRARY_PATH.patch \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    btor2tools.patch \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    googletest.patch
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-use_parallel_build  no
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+compiler.c_standard 1999
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+compiler.cxx_standard 2011
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-configure.pre_args
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+configure.args      -DBUILD_SHARED_LIBS=ON \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    -DUSE_GMP=ON \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    -DONLY_PICOSAT=ON \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                    -DPYTHON=OFF
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-destroot {
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -d ${destroot}${prefix}/share/doc/${name}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -m 755 -W ${worksrcpath} synthebtor deltabtor boolector \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${destroot}${prefix}/bin
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -m 644 ${worksrcpath}/boolector.h \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${destroot}${prefix}/include
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -m 644 ${worksrcpath}/libboolector.a \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${destroot}${prefix}/lib
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-    xinstall -m 644 -W ${worksrcpath} COPYING NEWS README VERSION \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-        ${destroot}${prefix}/share/doc/${name}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+test.run            yes
</span> 
<span style='display:block; white-space:pre;background:#ffe0e0;'>-livecheck.type      regex
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-livecheck.url       ${homepage}
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-livecheck.regex     boolector-(\[0-9\.\]+).tar.gz
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+post-destroot {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    set docdir ${prefix}/share/doc/${name}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    xinstall -d ${destroot}${docdir}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    xinstall -m 0644 -W ${worksrcpath} AUTHORS COPYING NEWS README.md \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+        ${destroot}${docdir}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+}
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/DYLD_LIBRARY_PATH.patch b/math/boolector/files/DYLD_LIBRARY_PATH.patch
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..1008bfbc986
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/boolector/files/DYLD_LIBRARY_PATH.patch
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,134 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+Set DYLD_LIBRARY_PATH so the test runners can find and use the library
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+that was just built.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- contrib/btorcheckmodel.py.orig 2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ contrib/btorcheckmodel.py      2022-01-06 09:52:14.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -14,14 +14,15 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   evalstring= "%0" + str(len) + "d"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   return evalstring % int(binary)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-if len(sys.argv) != 4:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  print("Usage: ./btorcheckmodel <btor-file> <btor-output-model-file> <boolector-binary>")
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++if len(sys.argv) != 5:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  print("Usage: ./btorcheckmodel <btor-file> <btor-output-model-file> <boolector-binary> <boolector-library-path>")
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   sys.exit(2)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ pid = os.getpid();
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ foutname = "/tmp/btorcheckmodel" + str(pid) +".btor"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # get absolute path to boolector binary
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ boolector = sys.argv[3]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++boolector_library_path = sys.argv[4]
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ def cleanup():
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -206,7 +207,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fout.write(str(id) + " root 1 -" + str(lastid) + "\n")
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ fout.close()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-ret = os.popen (boolector + " -rwl 0 " + foutname)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++ret = os.popen ("DYLD_LIBRARY_PATH=" + boolector_library_path + " " + boolector + " -rwl 0 " + foutname)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ result = ret.readline().strip()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if result == "sat":
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   print("Invalid")
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- contrib/btorcheckmodelsmt2.sh.orig     2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ contrib/btorcheckmodelsmt2.sh  2022-01-06 09:53:19.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -24,7 +24,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ do
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   case $1 in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     -h|--help)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-      echo -n "usage: $(basename $0) [<option>] <infile> <model> <boolector-binary>"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++      echo -n "usage: $(basename $0) [<option>] <infile> <model> <boolector-binary> <boolector-library-path>"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       echo
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       echo "  options:"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       echo "    -h, --help    print this message and exit"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -46,6 +46,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ MODEL="$1"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ BOOLECTOR="$2"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++BOOLECTOR_LIBRARY_PATH="$3"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ [ -z "$BOOLECTOR" ] && die "no Boolector binary specified"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ [ ! -e "$BOOLECTOR" ] && die "given Boolector binary does not exist"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -54,6 +55,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ cat $MODEL | sed 's/sat//' >> $TMPFILE
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ echo "(check-sat)" >> $TMPFILE
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ echo "(exit)" >> $TMPFILE
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++DYLD_LIBRARY_PATH="$BOOLECTOR_LIBRARY_PATH" \
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ "${BOOLECTOR}" ${TMPFILE}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ ret=$?
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ if [[ $ret = 10 ]]; then
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/CMakeLists.txt.orig       2022-01-06 08:01:44.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/CMakeLists.txt    2022-01-06 08:14:31.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -53,6 +53,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   target_link_libraries(test${test} GTest::gtest_main)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   set_target_properties(test${test} PROPERTIES OUTPUT_NAME test${test})
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   add_test(${test} ${CMAKE_BINARY_DIR}/bin/tests/test${test})
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  set_tests_properties(${test} PROPERTIES ENVIRONMENT DYLD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ endforeach()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set(sat_testcases
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -1019,6 +1019,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       ${RUN_TEST_CASE_SCRIPT}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       ${option}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       ${BOOLECTOR_BINARY}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++      ${CMAKE_BINARY_DIR}/lib
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       ${tcase}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       ${CMAKE_CURRENT_BINARY_DIR}
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   )
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/run-test-case.py.orig     2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/run-test-case.py  2022-01-06 10:14:19.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -47,6 +47,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     #print(sys.argv)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ap = argparse.ArgumentParser()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ap.add_argument('binary')
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++    ap.add_argument('library_path')
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ap.add_argument('testcase')
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ap.add_argument('output_dir')
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ap.add_argument('--check-sat', action='store_true', default=False)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -66,6 +67,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     print("Running test case '{}'".format(' '.join(cmd_args)))
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     proc = subprocess.Popen(cmd_args,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++                            env={'DYLD_LIBRARY_PATH': args.library_path},
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                             stdin=subprocess.PIPE,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                             stdout=subprocess.PIPE,
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+                             stderr=subprocess.PIPE)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/test_modelgen.cpp.orig    2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/test_modelgen.cpp 2022-01-06 09:56:27.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -13,6 +13,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btorconfig.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include <stdlib.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ class TestModelGen : public TestFile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+  protected:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -42,7 +44,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     std::stringstream ss_cmd;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ss_cmd << BTOR_CONTRIB_DIR << "btorcheckmodel.py " << BTOR_OUT_DIR << name
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            << ext << " " << d_log_file_name << " " << BTOR_BIN_DIR
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-           << "boolector > /dev/null";
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++           << "boolector " << getenv("DYLD_LIBRARY_PATH") << " > /dev/null";
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ret_val = system (ss_cmd.str ().c_str ());
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ASSERT_EQ (ret_val, 0);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #endif
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/test_modelgensmt2.cpp.orig        2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/test_modelgensmt2.cpp     2022-01-06 09:56:33.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -13,6 +13,8 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btorconfig.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ }
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include <stdlib.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ class TestModelGenSMT2 : public TestFile
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ {
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+  protected:
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -43,7 +45,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     std::stringstream ss_cmd;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ss_cmd << BTOR_CONTRIB_DIR << "btorcheckmodelsmt2.sh " << BTOR_OUT_DIR
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+            << name << ext << " " << d_log_file_name << " " << BTOR_BIN_DIR
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-           << "boolector > /dev/null";
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++           << "boolector " << getenv("DYLD_LIBRARY_PATH") << " > /dev/null";
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ret_val = system (ss_cmd.str ().c_str ());
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     ASSERT_EQ (ret_val, 0);
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #endif
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/btor2tools.patch b/math/boolector/files/btor2tools.patch
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..3ea6efb8c4c
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/boolector/files/btor2tools.patch
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,39 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+There is a discrepancy between where btor2tools installs its header and
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+where boolector is looking for it.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+boolector can download and build btor2tools for us, but we don't want
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+build systems to be downloading things for us, and we want to control
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+what flags are used for the build.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- cmake/FindBtor2Tools.cmake.orig        2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ cmake/FindBtor2Tools.cmake     2022-01-06 07:01:05.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -11,7 +11,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Btor2Tools_INCLUDE_DIR - the Btor2Tools include directory
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Btor2Tools_LIBRARIES - Libraries needed to use Btor2Tools
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-find_path(Btor2Tools_INCLUDE_DIR NAMES btor2parser/btor2parser.h)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++find_path(Btor2Tools_INCLUDE_DIR NAMES btor2parser.h)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ find_library(Btor2Tools_LIBRARIES NAMES btor2parser)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ include(FindPackageHandleStandardArgs)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/btormcmain.c.orig  2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/btormcmain.c       2022-01-06 07:00:38.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -9,7 +9,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "boolectormc.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btormc.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-#include "btor2parser/btor2parser.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include <btor2parser.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "utils/btorhashint.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "utils/btormem.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "utils/btoroptparse.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/parser/btorbtor2.c.orig    2021-05-27 19:47:11.000000000 -0500
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/parser/btorbtor2.c 2022-01-06 07:00:56.000000000 -0600
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -6,7 +6,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+  *  See COPYING for more information on using this software.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+  */
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-#include "btor2parser/btor2parser.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++#include <btor2parser.h>
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btormsg.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btorparse.h"
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #include "btortypes.h"
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/googletest.patch b/math/boolector/files/googletest.patch
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..c938b8aea65
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/math/boolector/files/googletest.patch
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,43 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+Don't download Google Test. Allow an already installed Google Test to be used.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+https://github.com/Boolector/boolector/commit/91533caf29a2c5b10b4912fd352e7af82c787598
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- CMakeLists.txt.orig
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ CMakeLists.txt
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -440,13 +440,6 @@ configure_file(
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #-----------------------------------------------------------------------------#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # Regression tests
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-# Get and configure google test
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-include(cmake/googletest.cmake)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-fetch_googletest(
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    ${PROJECT_SOURCE_DIR}/cmake
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    ${PROJECT_BINARY_DIR}/googletest
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-    )
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ enable_testing()
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #-----------------------------------------------------------------------------#
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ cmake/FindGoogleTest.cmake
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -0,0 +1,1 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++find_package(GTest 1.10.0)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- test/CMakeLists.txt.orig
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ test/CMakeLists.txt
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -5,6 +5,9 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # This file is part of Boolector.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ # See COPYING for more information on using this software.
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ #
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++find_package(GoogleTest REQUIRED)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/tests)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ 
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ set(test_names
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -47,7 +50,7 @@ foreach(test ${test_names})
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   add_executable (test${test} test_${test}.cpp)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   target_include_directories(test${test} PRIVATE ${PROJECT_SOURCE_DIR}/test/new_test)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   target_link_libraries(test${test} boolector m)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-  target_link_libraries(test${test} gtest_main)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++  target_link_libraries(test${test} GTest::gtest_main)
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   set_target_properties(test${test} PROPERTIES OUTPUT_NAME test${test})
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   add_test(${test} ${CMAKE_BINARY_DIR}/bin/tests/test${test})
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+ endforeach()
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/patch-btorexp.c.diff b/math/boolector/files/patch-btorexp.c.diff
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index d2e5d557df0..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/boolector/files/patch-btorexp.c.diff
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,11 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- work/boolector-1.4.1-376e6b0-110304/btorexp.c  2011-03-04 19:49:37.000000000 +0100
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ btorexp.c      2012-09-08 16:20:16.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -27,7 +27,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #include "btorconfig.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #include "btorexit.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #include "btorrewrite.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--#include "../picosat/picosat.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#include "picosat.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #include <stdlib.h>
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #include <stdio.h>
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/patch-btorsat.c.diff b/math/boolector/files/patch-btorsat.c.diff
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index ad149c88dea..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/boolector/files/patch-btorsat.c.diff
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,15 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- work/boolector-1.4.1-376e6b0-110304/btorsat.c  2010-06-14 18:38:20.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ btorsat.c      2012-09-08 16:20:41.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -17,10 +17,10 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-  *  along with this program.  If not, see <http://www.gnu.org/licenses/>.
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-  */
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--#include "../picosat/picosat.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#include "picosat.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #ifdef BTOR_USE_PICOPREP
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--#include "../picoprep/picoprep.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+#include "picoprep.h"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #endif
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- #ifdef BTOR_USE_PRECOSAT
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/patch-configure.diff b/math/boolector/files/patch-configure.diff
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 5fc5d6401f4..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/boolector/files/patch-configure.diff
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,25 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- work/boolector-1.4.1-376e6b0-110304/configure  2010-05-14 15:52:49.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ configure      2012-09-08 16:44:05.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -23,11 +23,6 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-  [ -f $1 ] || die "can not find '$1'" 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- }
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--check ../picosat/picosat.h
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--check ../picosat/version.o
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--check ../picosat/picosat.o
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--echo "picosat backend"
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- if [ $precosat = yes ]
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- then
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   check ../precosat/precosat.hh
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -58,8 +53,8 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- rm -f makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- sed \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -e "s,@CC@,$CC," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---e "s,@CFLAGS@,$CFLAGS," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---e "s,@LIBS@,$LIBS," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+-e "s,@CFLAGS@,$CFLAGS $CPPFLAGS," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+-e "s,@LIBS@,$LDFLAGS -lpicosat $LIBS," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- -e "s,@PRECOSAT@,$PRECOSAT," \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- makefile.in > makefile
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- 
</span><span style='display:block; white-space:pre;color:#808080;'>diff --git a/math/boolector/files/patch-makefile.in.diff b/math/boolector/files/patch-makefile.in.diff
</span>deleted file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 1cb0ba0ff24..00000000000
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/math/boolector/files/patch-makefile.in.diff
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -1,11 +0,0 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>---- work/boolector-1.4.1-376e6b0-110304/makefile.in        2011-03-04 19:52:48.000000000 +0100
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+++ makefile.in    2012-09-08 16:45:41.000000000 +0200
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-@@ -4,7 +4,7 @@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- .cc.o:
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-   $(CC) $(CFLAGS) -c $<
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- OBJ=boolector.o $(addsuffix .o,$(basename $(wildcard btor*.c))) \
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--  ../picosat/picosat.o ../picosat/version.o @PRECOSAT@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>-+  @PRECOSAT@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CC=@CC@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- CFLAGS=@CFLAGS@
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>- LIBS=@LIBS@
</span></pre><pre style='margin:0'>

</pre>