cvc4 linking problem

cvc4 problem

only there to have a better name in the overview

inter.cc

#include <cvc4/cvc4.h>

int main() {
  CVC4::ExprManager _manager;
  CVC4::SmtEngine _engine(& _manager);
  _engine.setLogic("UFLIA");

  CVC4::Integer i = CVC4::Integer(1000);

  _manager.mkConst(i);
  
  return 0;
}

Makefile

CC=g++
CFLAGS=-I /opt/cvc4-devel/include
LFLAGS=-L /opt/cvc4-devel/lib
LIBS=-lcvc4 -lgmp

all : inter

inter : inter.o
	$(CC) $(LFLAGS) -o inter inter.o $(LIBS)

inter.o : inter.cc
	$(CC) -c $(CFLAGS) inter.cc

clean :
	rm inter
	rm *.o

Compilation is accepted, but linking is not:

make 
g++ -c -I /opt/cvc4-devel/include inter.cc
g++ -L /opt/cvc4-devel/lib -o inter inter.o -lcvc4 -lgmp
inter.o: In function `main':
inter.cc:(.text+0x75): undefined reference to `CVC4::Expr CVC4::ExprManager::mkConst<CVC4::Integer>(CVC4::Integer const&)'
collect2: error: ld returned 1 exit status
make: *** [Makefile:9: inter] Error 1

I believe this is due to the declaration of a generic mkConst in expr_manager.h :

  /** Create a constant of type T */
  template <class T>
  Expr mkConst(const T&);

even though the template is not instantiated for the Integer class. The actual libcvc4.so only contains the instantiated templates which would explain that the error only occurs at the linking stage.

CVC4::Rational covers both integers and rationals, the proper call would be mkConst(CVC4::Rational(1000)).