vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

Vampire crashing when printing a finite model: #565

Open quickbeam123 opened 3 months ago

quickbeam123 commented 3 months ago
$ ./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 commented 3 months ago

Probably a duplicate of https://github.com/vprover/vampire/issues/461