Неопределенные ссылочные ошибки при компиляции примера кода z3 - PullRequest
Новая
       15

Неопределенные ссылочные ошибки при компиляции примера кода z3

2 голосов
/ 04 июня 2019

Я установил Z3 и смог скомпилировать примеры C / C ++, а также примеры make.Но когда я пытаюсь скомпилировать любой пример кода, включив в него «z3 ++. H» и используя также флаг компоновщика lz3, я получаю неопределенные ошибки ссылок.

Когда я установил Z3 и скомпилировал тот же код ранее, это сработало.Я не вносил никаких изменений в код Z3, но теперь он выдает неожиданные ошибки.

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

Ошибки: test.o: в функции `z3 :: operator + (z3 :: expr const &, z3 :: expr const &) ': test.cpp: (. .cpp :( text._ZN2z36concatERKNS_4exprES2 _ [_ ZN2z36concatERKNS_4exprES2 _] + 0x76): 'test.cpp :( text._ZN2z36concatERKNS_4exprES2 _ [_ ZN2z36concatERKNS_4exprES2 _] + 0xd3): неопределенная ссылка на `Z3_mk_seq_concat' неопределенная ссылка на` Z3_is_seq_sort. test.cpp :( текст._ZN2z36concatERKNS_4exprES2 _ [_ _ ZN2z36concatERKNS_4exprES2] + 0x11d): не определена ссылка на `Z3_is_re_sort 'test.cpp :( text._ZN2z36concatERKNS_4exprES2 _ [_ _] ZN2z36concatERKNS_4exprES2 + 0x17a):. неопределенная ссылка на` Z3_mk_re_concat' collect2: ошибка: LD возвращается 1 выход статуса

...