2

I installed Z3 and was able to compile C/C++ examples as well with make examples. But when I try to compile any sample code by including "z3++.h" and using lz3 linker flag as well, I get undefined reference errors.

When I installed Z3 and compiled same code earlier, it worked. I didn't make any changes in Z3 code, but now it throws unexpected errors.

cat test.cpp

#include<z3++.h>
using namespace z3;

int main() {
    context c;
    expr x = c.int_const("x");
    std::cout << x + 1 << "\n";
    return 0;
}

g++ -c test.cpp

g++ -o test test.o -lz3

Errors: test.o: In function `z3::operator+(z3::expr const&, z3::expr const&)': test.cpp:(.text._ZN2z3plERKNS_4exprES2_[_ZN2z3plERKNS_4exprES2_]+0x203): undefined reference to `Z3_mk_re_union' test.o: In function `z3::concat(z3::expr const&, z3::expr const&)': test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x76): undefined reference to `Z3_is_seq_sort' test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0xd3): undefined reference to `Z3_mk_seq_concat' test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x11d): undefined reference to `Z3_is_re_sort' test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x17a): undefined reference to `Z3_mk_re_concat' collect2: error: ld returned 1 exit status

dustinos3
  • 934
  • 3
  • 17
  • 27
harsha
  • 21
  • 4
  • Possible duplicate of [What is an undefined reference/unresolved external symbol error and how do I fix it?](https://stackoverflow.com/questions/12573816/what-is-an-undefined-reference-unresolved-external-symbol-error-and-how-do-i-fix) – Ken White Jun 04 '19 at 16:38
  • I understand the problem. I want to ask the solution which is more related to linking Z3 library. – harsha Jun 04 '19 at 17:37
  • Works fine for me exactly with those commands; must be something wrong with your installation. – alias Jun 04 '19 at 18:22
  • We can't possibly provide a specific solution for every possible unresolved external for every possible project or app or library. Search the existing posts for related errors and use the information you find there to resolve the issue you're experiencing. Try a search for the exact phrase (including the brackets) `[z3] undefined reference` – Ken White Jun 04 '19 at 20:15
  • @KenWhite please be nicer to new contributors. Z3 is popular enough to have its own tag and users who provide support for it. – ahelwer Jun 04 '19 at 21:07
  • @ahelwer: No one is not being nice. There are many existing questions tagged [tag:z3] that deal with unresolved external references. New user or not, posters are expected to search existing posts for possible solutions before posting a new question. – Ken White Jun 04 '19 at 23:42
  • Thank you for your answers. But I did search for all available answers on Stack Overflow related to this before posting my question. I followed all steps given in Readme for installation of Z3 and did not get any errors in any of the steps so I don't really get what could be wrong with my installation ? – harsha Jun 05 '19 at 02:02
  • Strangely enough, Reinstalling library libz3-dev worked for me. Thanks. – harsha Jun 05 '19 at 05:45

1 Answers1

1

late answer but i think you should add the "-lz3" flag to your build command.

M.Noe
  • 58
  • 4