Skip to content
New issue

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 crashing when printing a finite model: #565

Open
quickbeam123 opened this issue May 30, 2024 · 1 comment
Open

Vampire crashing when printing a finite model: #565

quickbeam123 opened this issue May 30, 2024 · 1 comment

Comments

@quickbeam123
Copy link
Collaborator

quickbeam123 commented May 30, 2024

$ ./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.)

@quickbeam123
Copy link
Collaborator Author

Probably a duplicate of #461

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant