<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>