Skip to content

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

Closed
jmony opened this issue May 15, 2020 · 4 comments · Fixed by #5549
Closed

Cannot build with IPASIR - cryptominisat #5345

jmony opened this issue May 15, 2020 · 4 comments · Fixed by #5549

Comments

@jmony
Copy link

jmony commented May 15, 2020

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'

@jmony
Copy link
Author

jmony commented May 15, 2020

I forgot to mention that I edited config.inc to uncomment IPASIR (and only IPASIR).

@peterschrammel
Copy link
Member

This might be fixed by #5305.

@jmony
Copy link
Author

jmony commented May 15, 2020

I tried with #5305 but it had no effect.

@tautschnig
Copy link
Collaborator

I actually messed this up in 89641a2. We'll need #5305 (or some variant thereof) plus an additional fix.

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
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants