satcheck_minisat2.cpp: error: 'l_True' was not declared in this scope; did you mean 'Minisat::l_True'?

[vt-alt]

When building CBMC version 5.95.1 with system provided minisat (-Dsat_impl="system-minisat2"), build fails with:

[00:00:39] [ 35%] Building CXX object src/solvers/CMakeFiles/solvers.dir/sat/satcheck_minisat2.cpp.o
[00:00:39] cd /usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src/solvers && /usr/bin/c++ -DHAVE_MINISAT2 -DSATCHECK_MINISAT2 -I/usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src -I/usr/src/RPM/BUILD/cbmc-5.95.1/src -I/usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src/solvers -I/usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers -I/usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src/util -I/usr/src/RPM/BUILD/cbmc-5.95.1/src/util -I/usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src/big-int -I/usr/src/RPM/BUILD/cbmc-5.95.1/src/big-int -I/usr/src/RPM/BUILD/cbmc-5.95.1/x86_64-alt-linux/src/langapi -I/usr/src/RPM/BUILD/cbmc-5.95.1/src/langapi -pipe -frecord-gcc-switches -Wall -g -O2   -Wno-error=odr -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum -O2 -std=gnu++11 -MD -MT src/solvers/CMakeFiles/solvers.dir/sat/satcheck_minisat2.cpp.o -MF CMakeFiles/solvers.dir/sat/satcheck_minisat2.cpp.o.d -o CMakeFiles/solvers.dir/sat/satcheck_minisat2.cpp.o -c /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp: In member function 'tvt satcheck_minisat2_baset<T>::l_get(literalt) const':
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:71:33: error: 'l_True' was not declared in this scope; did you mean 'Minisat::l_True'?
[00:00:39]    71 |   if(solver->model[a.var_no()]==l_True)
[00:00:39]       |                                 ^~~~~~
[00:00:39]       |                                 Minisat::l_True
[00:00:39] In file included from /usr/include/minisat/core/Solver.h:29,
[00:00:39]                  from /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:22:
[00:00:39] /usr/include/minisat/core/SolverTypes.h:128:15: note: 'Minisat::l_True' declared here
[00:00:39]   128 |   const lbool l_True ((uint8_t)0);
[00:00:39]       |               ^~~~~~
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:73:38: error: 'l_False' was not declared in this scope; did you mean 'Minisat::l_False'?
[00:00:39]    73 |   else if(solver->model[a.var_no()]==l_False)
[00:00:39]       |                                      ^~~~~~~
[00:00:39]       |                                      Minisat::l_False
[00:00:39] /usr/include/minisat/core/SolverTypes.h:129:15: note: 'Minisat::l_False' declared here
[00:00:39]   129 |   const lbool l_False((uint8_t)1);
[00:00:39]       |               ^~~~~~~
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp: In member function 'void satcheck_minisat2_baset<T>::set_polarity(literalt, bool)':
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:94:45: error: 'l_True' was not declared in this scope; did you mean 'Minisat::l_True'?
[00:00:39]    94 |     solver->setPolarity(a.var_no(), value ? l_True : l_False);
[00:00:39]       |                                             ^~~~~~
[00:00:39]       |                                             Minisat::l_True
[00:00:39] /usr/include/minisat/core/SolverTypes.h:128:15: note: 'Minisat::l_True' declared here
[00:00:39]   128 |   const lbool l_True ((uint8_t)0);
[00:00:39]       |               ^~~~~~
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:94:54: error: 'l_False' was not declared in this scope; did you mean 'Minisat::l_False'?
[00:00:39]    94 |     solver->setPolarity(a.var_no(), value ? l_True : l_False);
[00:00:39]       |                                                      ^~~~~~~
[00:00:39]       |                                                      Minisat::l_False
[00:00:39] /usr/include/minisat/core/SolverTypes.h:129:15: note: 'Minisat::l_False' declared here
[00:00:39]   129 |   const lbool l_False((uint8_t)1);
[00:00:39]       |               ^~~~~~~
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp: In member function 'propt::resultt satcheck_minisat2_baset<T>::do_prop_solve(const bvt&)':
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:274:25: error: 'l_True' was not declared in this scope; did you mean 'Minisat::l_True'?
[00:00:39]   274 |     if(solver_result == l_True)
[00:00:39]       |                         ^~~~~~
[00:00:39]       |                         Minisat::l_True
[00:00:39] /usr/include/minisat/core/SolverTypes.h:128:15: note: 'Minisat::l_True' declared here
[00:00:39]   128 |   const lbool l_True ((uint8_t)0);
[00:00:39]       |               ^~~~~~
[00:00:39] /usr/src/RPM/BUILD/cbmc-5.95.1/src/solvers/sat/satcheck_minisat2.cpp:282:25: error: 'l_False' was not declared in this scope; did you mean 'Minisat::l_False'?
[00:00:39]   282 |     if(solver_result == l_False)
[00:00:39]       |                         ^~~~~~~
[00:00:39]       |                         Minisat::l_False
[00:00:39] /usr/include/minisat/core/SolverTypes.h:129:15: note: 'Minisat::l_False' declared here
[00:00:39]   129 |   const lbool l_False((uint8_t)1);
[00:00:39]       |               ^~~~~~~
[00:00:39] gmake[2]: *** [src/solvers/CMakeFiles/solvers.dir/build.make:1994: src/solvers/CMakeFiles/solvers.dir/sat/satcheck_minisat2.cpp.o] Error 1

Adding -DMINISAT_CONSTANTS_AS_MACROS to the CXXFLAGS solves the issue. Perhaps this should be auto-added or constants namespaced.

CBMC version: 5.95.1
Operating system: ALT Linux
Exact command line resulting in the issue:

[00:00:04] + cmake -DCMAKE_SKIP_INSTALL_RPATH:BOOL=yes '-DCMAKE_C_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -Wno-error=odr' '-DCMAKE_CXX_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -Wno-error=odr' '-DCMAKE_Fortran_FLAGS:STRING=-pipe -frecord-gcc-switches -Wall -g -O2   -Wno-error=odr' -DCMAKE_INSTALL_PREFIX=/usr -DINCLUDE_INSTALL_DIR:PATH=/usr/include -DLIB_INSTALL_DIR:PATH=/usr/lib64 -DSYSCONF_INSTALL_DIR:PATH=/etc -DSHARE_INSTALL_PREFIX:PATH=/usr/share -DLIB_DESTINATION=lib64 -DLIB_SUFFIX=64 -S . -B x86_64-alt-linux -DWITH_JBMC:BOOL=OFF -DBUILD_SHARED_LIBS:BOOL=OFF -Dsat_impl=system-minisat2
[00:00:05] + cmake --build x86_64-alt-linux --verbose --parallel 32

[esteffin]

Hi @vt-alt, I had an investigation at your problem.

Essentially it looks like that after minisat version 2.2.0, which is the last official release (according to minisat github repo), some extra commits have been added to the repository.
Some Linux distros (like ALT) have minisat version 2.2.1 in their repositories which contains such changes.

One of such commits (here) changes the way symbols l_True and l_False are defined.

Here I agree that adding -DMINISAT_CONSTANTS_AS_MACROS is the best approach as it will be compatible with all versions including our patched minisat (used as default).

@tautschnig as you introduced the system-minisat2 option, do you agree?

[kroening]

Given that Minisat hasn't changed for a decade, I'd like to suggest to import the source into the CBMC repo

[vt-alt]

@esteffin Thanks!

There is maintained fork at https://github.com/stp/minisat even though there isn't very big code difference and mostly cmake builds updates.

From distribution point of view linking with external shared library is preferable than embedding (vendoring or even static linking).

[tautschnig]

@vt-alt Could you please give the patch from #8107 a try and report back whether that fixes all issues for you? Thank you!

[vt-alt]

@tautschnig I just tested compiling cbmc 5.95.1 release on ALT with this PR #8107 applied over it (without -DMINISAT_CONSTANTS_AS_MACROS) and build is successful. Thanks!