Skolemization violates its own invariant

Failed: ModelExpansion/MXsatTest.DoesSatMXSkolemize/19
Testing /home/bartb/software/idp/tests/mx/satmx/SATdfasat.idp
stack trace:
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : AssertionException::AssertionException(std::string)+0x58
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : Skolemize::visit(QuantForm*)+0x101
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : QuantForm::accept(TheoryMutatingVisitor*)+0x2e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : TheoryMutatingVisitor::traverse(Formula*)+0xc7
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : TheoryMutatingVisitor::visit(BoolForm*)+0x2e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : BoolForm::accept(TheoryMutatingVisitor*)+0x2e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : TheoryMutatingVisitor::traverse(Formula*)+0xc7
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : Skolemize::visit(QuantForm*)+0x188
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : QuantForm::accept(TheoryMutatingVisitor*)+0x2e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : Skolemize::visit(Theory*)+0xe2
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : Theory::accept(TheoryMutatingVisitor*)+0x2e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : AbstractTheory* Skolemize::execute<AbstractTheory*>(AbstractTheory*, Vocabulary*)+0x41
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : _Z9transformI9SkolemizeP14AbstractTheoryS1_IP10VocabularyEET0_PT1_DpT2_()+0x127
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : FormulaUtils::skolemize(AbstractTheory*)+0x2a
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : AbstractTheory* FormulaUtils::improveTheoryForInference<AbstractTheory*>(AbstractTheory*, Structure*, bool, bool)+0xbc
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : GrounderFactory::ground(AbstractTheory*, Term*)+0x9c
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : LazyGroundingManager* GrounderFactory::createGrounder<GroundTheory<SolverPolicy<MinisatID::Space> >*>(GroundInfo const&, GroundTheory<SolverPolicy<MinisatID::Space> >*)+0x318
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : GrounderFactory::create(GroundInfo const&, MinisatID::Space*)+0xcb
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : GroundingInference<MinisatID::Space>::ground()+0xd9e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : GroundingInference<MinisatID::Space>::createGroundingAndExtender(AbstractTheory*, Structure*, Vocabulary*, Term*, TraceMonitor*, bool, MinisatID::Space*)+0x263
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : ModelExpansion::expand() const+0x3da
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : ModelExpansion::doModelExpansion(AbstractTheory*, Structure*, Vocabulary*, TraceMonitor*, MXAssumptions const&)+0x6e
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : executeMXCommand(AbstractTheory*, Structure*, Vocabulary*)+0xe2
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : ModelExpandInference::execute(std::__debug::vector<InternalArgument, std::allocator<InternalArgument> > const&) const+0x55
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : LuaConnection::InternalProcedure::operator()(lua_State*) const+0x11a
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : LuaConnection::internalCall(lua_State*)+0x64a
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x13f7f
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x2b77a
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x14251
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x96b2
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x1318e
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : ()+0x1467d
  /cw/dtailocal/bartb/builds/idp/debug/lib/lua/src/liblua.so.5 : lua_pcall(lua_State*, int, int, int)+0xa8
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : LuaConnection::execute(std::string const&)+0x57
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : Insert::exec(std::string const&)+0x18
  /cw/dtailocal/bartb/builds/idp/debug/src/libidp.so : handleAndRun(void*)+0x29
  /cw/dtailocal/bartb/builds/idp/debug/lib/tinythread/source/libtinythread.so : tthread::thread::wrapper_function(void*)+0x29
  /lib/x86_64-linux-gnu/libpthread.so.0 : ()+0x7e9a
  /lib/x86_64-linux-gnu/libc.so.6 : clone()+0x6d
Error: ASSERT FAILED: qf->sign()==SIGN::POS @ /home/bartb/software/idp/src/theory/transformations/Skolemize.hpp (71)
/home/bartb/software/idp/tests/TestUtils.cpp:30: Failure
Value of: result
  Actual: failed
Expected: Status::SUCCESS
Which is: success
Comments (0)
