We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
$ ./vampire_dbg_master_7630 -sa fmb Problems/ITP/ITP383_10.p --traceback on % Running in auto input_syntax mode. Trying TPTP TRYING [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1] Finite Model Found! % SZS status Satisfiable for ITP383_10 Condition in file ./Lib/DHMap.hpp, line 193 violated: e ----- stack dump ----- Version : Vampire 4.8 (commit d71672a8c on 2024-05-20 12:15:43 +0200) call stack: 0x6 0x7fff2063ef3d 0x100737119 0x100735960 0x1007348de 0x100731fd3 0x10045ac7d 0x10045af04 0x1000f2a5b 0x100698da3 0x10069cb7a 0x100385403 0x100020858 0x1000234a5 invoking atos(1) ... 0x6 0x7fff2063ef3d main (in vampire_dbg_master_7630) (vampire.cpp:795) dispatchByMode(Kernel::Problem*) (in vampire_dbg_master_7630) (vampire.cpp:560) vampireMode(Kernel::Problem*) (in vampire_dbg_master_7630) (vampire.cpp:366) doProving(Kernel::Problem*) (in vampire_dbg_master_7630) (vampire.cpp:158) Saturation::ProvingHelper::runVampireSaturation(Kernel::Problem&, Shell::Options const&) (in vampire_dbg_master_7630) (ProvingHelper.cpp:55) Saturation::ProvingHelper::runVampireSaturationImpl(Kernel::Problem&, Shell::Options const&) (in vampire_dbg_master_7630) (ProvingHelper.cpp:143) Kernel::MainLoop::run() (in vampire_dbg_master_7630) (MainLoop.cpp:58) FMB::FiniteModelBuilder::runImpl() (in vampire_dbg_master_7630) (FiniteModelBuilder.cpp:1710) FMB::FiniteModelBuilder::onModelFound() (in vampire_dbg_master_7630) (FiniteModelBuilder.cpp:2258) Lib::DHMap<unsigned int, unsigned int, Lib::DefaultHash, Lib::DefaultHash2>::get(unsigned int) (in vampire_dbg_master_7630) (DHMap.hpp:194) Debug::Assertion::violated(char const*, int, char const*) (in vampire_dbg_master_7630) (Assertion.cpp:50) Debug::Tracer::printStack(std::__1::basic_ostream<char, std::__1::char_traits<char> >&) (in vampire_dbg_master_7630) (Tracer.cpp:51) ----- end of stack dump -----
(This turns into a segfault in Release.)
The text was updated successfully, but these errors were encountered:
Probably a duplicate of #461
Sorry, something went wrong.
No branches or pull requests
(This turns into a segfault in Release.)
The text was updated successfully, but these errors were encountered: