You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
I have encountered an issue to build v3. Thanks. I am using ubuntu 18.04 and g++-5.
The text was updated successfully, but these errors were encountered: