-
Notifications
You must be signed in to change notification settings - Fork 274
Cannot build with IPASIR - cryptominisat #5345
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
I forgot to mention that I edited config.inc to uncomment IPASIR (and only IPASIR). |
This might be fixed by #5305. |
I tried with #5305 but it had no effect. |
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 6, 2020
Hardness support was added to minisat2 only, and 89641a2 failed to update the IPASIR interface. Also cleanup the list of phony targets in the top-level Makefile, and ensure that linking of the memory analyzer succeeds even in presence of LIBS set on the make command line. Fixes: diffblue#5345
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
Nov 6, 2020
Hardness support was added to minisat2 only, and 89641a2 failed to update the IPASIR interface. Also cleanup the list of phony targets in the top-level Makefile, and ensure that linking of the memory analyzer succeeds even in presence of LIBS set on the make command line. Fixes: diffblue#5345
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
CBMC version: master and Release 5.12
Operating system: Linux (Debian and Ubuntu)
Exact command line resulting in the issue: make -C src IPASIR=/home/ubuntu/cryptominisat/src LIBS="/home/ubuntu/cryptominisat/build/lib/libipasircryptominisat5.a"
(cryptominisat built OK)
What behaviour did you expect: Successful build
What happened instead:
Entering solvers
make -C solvers
make[1]: Entering directory '/home/ubuntu/cbmc-cbmc-5.12/src/solvers'
g++ -c -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -MMD -MP -std=c++11 -O2 -DHAVE_IPASIR -I .. -I /home/ubuntu/cryptominisat/src -o sat/satcheck_ipasir.o sat/satcheck_ipasir.cpp
sat/satcheck_ipasir.cpp: In constructor ‘satcheck_ipasirt::satcheck_ipasirt()’:
sat/satcheck_ipasir.cpp:161:36: error: no matching function for call to ‘cnf_solvert::cnf_solvert()’
satcheck_ipasirt::satcheck_ipasirt()
^
In file included from sat/satcheck_ipasir.h:15:0,
from sat/satcheck_ipasir.cpp:20:
sat/cnf.h:72:12: note: candidate: cnf_solvert::cnf_solvert(message_handlert&)
explicit cnf_solvert(message_handlert &message_handler)
^~~~~~~~~~~
sat/cnf.h:72:12: note: candidate expects 1 argument, 0 provided
sat/cnf.h:69:7: note: candidate: cnf_solvert::cnf_solvert(const cnf_solvert&)
class cnf_solvert:public cnft
^~~~~~~~~~~
sat/cnf.h:69:7: note: candidate expects 1 argument, 0 provided
sat/cnf.h:69:7: note: candidate: cnf_solvert::cnf_solvert(cnf_solvert&&)
sat/cnf.h:69:7: note: candidate expects 1 argument, 0 provided
../common:222: recipe for target 'sat/satcheck_ipasir.o' failed
make[1]: *** [sat/satcheck_ipasir.o] Error 1
make[1]: Leaving directory '/home/ubuntu/cbmc-cbmc-5.12/src/solvers'
Makefile:97: recipe for target 'solvers.dir' failed
make: *** [solvers.dir] Error 2
make: Leaving directory '/home/ubuntu/cbmc-cbmc-5.12/src'
The text was updated successfully, but these errors were encountered: