I have encountered an issue to build v3. Thanks. I am using ubuntu 18.04 and g++-5.
building v3...
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function rl_username_completion_function': (.text+0x4419): warning: Using 'getpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(tilde.o): In function
tilde_expand_word':
(.text+0x134): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(shell.o): In function sh_get_home_dir': (.text+0x109): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking /usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function
rl_username_completion_function':
(.text+0x440f): warning: Using 'setpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
(.text+0x44a9): warning: Using 'endpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::solve()': v3SvrMiniSat.cpp:(.text+0x1d3): undefined reference to
Solver::solve_()'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setImplyInit()': v3SvrMiniSat.cpp:(.text+0x465): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x5e8): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::newVar(unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x814): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::assertProperty(unsigned long const&, bool const&)':
v3SvrMiniSat.cpp:(.text+0x1123): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::assertProperty(V3NetId const&, bool const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x11db): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::assump_solve()':
v3SvrMiniSat.cpp:(.text+0x1292): undefined reference to Solver::solve_()' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::setTargetValue(V3NetId const&, V3BitVecX const&, unsigned int const&, unsigned long const&)':
v3SvrMiniSat.cpp:(.text+0x1445): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x14d5): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x1529): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x1593): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x15ed): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x1645): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x1699): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::setImplyIntersection(std::vector<unsigned long, std::allocator > const&)':
v3SvrMiniSat.cpp:(.text+0x1851): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x1955): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertInit()': v3SvrMiniSat.cpp:(.text+0x1c54): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::assertImplyUnion(std::vector<unsigned long, std::allocator<unsigned long> > const&)': v3SvrMiniSat.cpp:(.text+0x1d9e): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::setImplyUnion(std::vector<unsigned long, std::allocator<unsigned long> > const&)': v3SvrMiniSat.cpp:(.text+0x1ee5): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x1fb6): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_FALSE_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x2066): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x20d6): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_PI_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2154): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_AND_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2225): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_XOR_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2425): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_MUX_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x2626): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_RED_AND_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x28de): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x29fe): more undefined references to Solver::newVar(lbool, bool)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_CONST_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x3bed): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_SLICE_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x3e45): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x3f55): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_MERGE_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x4065): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_EQUALITY_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x42b5): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_GEQ_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x44dc): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x4646): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x468e): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x46f9): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x480d): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x4863): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x48bb): more undefined references to
Solver::addClause_(vec<Lit, int>&)' follow
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHL_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x530a): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x5523): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x55bd): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x565b): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x58de): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x59ce): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x5abe): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x5ba6): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_SHL_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x6399): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x654f): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_SHR_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x6714): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x692f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x69cc): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x6a6d): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x6c8e): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x6d7e): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x6e6d): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x6f56): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_SHR_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x7799): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7958): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_DIV_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0x7a05): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x7c5f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7cb6): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x7e64): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x7fa5): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x8096): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x81e5): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x82d6): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x8425): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x8516): more undefined references to Solver::addClause_(vec<Lit, int>&)' follow ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::add_MODULO_Formula(V3NetId const&, unsigned int const&)':
v3SvrMiniSat.cpp:(.text+0x8fe7): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x9240): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x928f): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0x944b): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0x9585): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x9676): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x97b5): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text+0x98a6): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text+0x99e5): undefined reference to Solver::addClause_(vec<Lit, int>&)' ../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text+0x9ad6): more undefined references to
Solver::addClause_(vec<Lit, int>&)' follow
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::add_FF_Formula(V3NetId const&, unsigned int const&)': v3SvrMiniSat.cpp:(.text+0xa5b4): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0xa645): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0xa755): undefined reference to
Solver::newVar(lbool, bool)'
v3SvrMiniSat.cpp:(.text+0xa8a4): undefined reference to Solver::newVar(lbool, bool)' v3SvrMiniSat.cpp:(.text+0xaa5a): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::reset()': v3SvrMiniSat.cpp:(.text+0xab61): undefined reference to
Solver::Solver()'
v3SvrMiniSat.cpp:(.text+0xabbf): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::V3SvrMiniSat(V3Ntk const*, bool const&)':
v3SvrMiniSat.cpp:(.text+0xaeca): undefined reference to Solver::Solver()' v3SvrMiniSat.cpp:(.text+0xaefc): undefined reference to
Solver::newVar(lbool, bool)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function V3SvrMiniSat::V3SvrMiniSat(V3SvrMiniSat const&)': v3SvrMiniSat.cpp:(.text+0xb1af): undefined reference to
Solver::Solver()'
v3SvrMiniSat.cpp:(.text+0xb1e1): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::simplify()':
v3SvrMiniSat.cpp:(.text+0x175): undefined reference to Solver::simplify()' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
V3SvrMiniSat::reserveFormula()':
v3SvrMiniSat.cpp:(.text.ZN12V3SvrMiniSat14reserveFormulaEv[ZN12V3SvrMiniSat14reserveFormulaEv]+0x1d): undefined reference to Solver::newVar(lbool, bool)' ../../lib/libsvr.a(v3SvrMiniSat.o): In function
void buf(Solver*, Lit const&, Lit const&)':
v3SvrMiniSat.cpp:(.text.Z3bufI6SolverEvPT_RK3LitS5[Z3bufI6SolverEvPT_RK3LitS5]+0x83): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text._Z3bufI6SolverEvPT_RK3LitS5_[_Z3bufI6SolverEvPT_RK3LitS5_]+0xc9): undefined reference to
Solver::addClause(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o): In function void xor_2<Solver>(Solver*, Lit const&, Lit const&, Lit const&)': v3SvrMiniSat.cpp:(.text._Z5xor_2I6SolverEvPT_RK3LitS5_S5_[_Z5xor_2I6SolverEvPT_RK3LitS5_S5_]+0x9e): undefined reference to
Solver::addClause(vec<Lit, int>&)'
v3SvrMiniSat.cpp:(.text.Z5xor_2I6SolverEvPT_RK3LitS5_S5[Z5xor_2I6SolverEvPT_RK3LitS5_S5]+0x106): undefined reference to Solver::addClause_(vec<Lit, int>&)' v3SvrMiniSat.cpp:(.text._Z5xor_2I6SolverEvPT_RK3LitS5_S5_[_Z5xor_2I6SolverEvPT_RK3LitS5_S5_]+0x159): undefined reference to
Solver::addClause_(vec<Lit, int>&)'
../../lib/libsvr.a(v3SvrMiniSat.o):v3SvrMiniSat.cpp:(.text.Z5xor_2I6SolverEvPT_RK3LitS5_S5[Z5xor_2I6SolverEvPT_RK3LitS5_S5]+0x1ac): more undefined references to `Solver::addClause_(vec<Lit, int>&)' follow
collect2: error: ld returned 1 exit status
Makefile:11: recipe for target '../../v3' failed
make[1]: *** [../../v3] Error 1