search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

--slack-level test failure #257

Closed soonhokong closed 8 years ago

soonhokong commented 8 years ago 
$ ./dReal ../../src/tests/nra/dzufferey_01.smt2 --slack-level 1
Assertion failed: (car->isTerm( ) || car->isSymb( ) || car->isNumb( )), function cons, file /Users/soonhok/work/dreal3/src/opensmt/egraph/EgraphStore.C, line 524.
[1]    20997 abort      ./dReal ../../src/tests/nra/dzufferey_01.smt2 --slack-level 1
$ lldb ./dReal
(lldb) target create "./dReal"
Current executable set to './dReal' (x86_64).
(lldb) run ../../src/tests/nra/dzufferey_01.smt2 --slack-level 1
Process 21166 launched: './dReal' (x86_64)
Assertion failed: (car->isTerm( ) || car->isSymb( ) || car->isNumb( )), function cons, file /Users/soonhok/work/dreal3/src/opensmt/egraph/EgraphStore.C, line 524.
Process 21166 stopped
* thread #1: tid = 0x2eb49, 0x00007fff906f9f06 libsystem_kernel.dylib`__pthread_kill + 10, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
    frame #0: 0x00007fff906f9f06 libsystem_kernel.dylib`__pthread_kill + 10
libsystem_kernel.dylib`__pthread_kill:
->  0x7fff906f9f06 <+10>: jae    0x7fff906f9f10            ; <+20>
    0x7fff906f9f08 <+12>: movq   %rax, %rdi
    0x7fff906f9f0b <+15>: jmp    0x7fff906f47cd            ; cerror_nocancel
    0x7fff906f9f10 <+20>: retq
(lldb) bt
* thread #1: tid = 0x2eb49, 0x00007fff906f9f06 libsystem_kernel.dylib`__pthread_kill + 10, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
  * frame #0: 0x00007fff906f9f06 libsystem_kernel.dylib`__pthread_kill + 10
    frame #1: 0x00007fff9c9864ec libsystem_pthread.dylib`pthread_kill + 90
    frame #2: 0x00007fff8cd536e7 libsystem_c.dylib`abort + 129
    frame #3: 0x00007fff8cd1adf8 libsystem_c.dylib`__assert_rtn + 321
    frame #4: 0x00000001000af2c8 dReal`Egraph::cons(this=0x0000000102808200, car=0x0000000100d07e30, cdr=0x0000000100d08040) + 296 at EgraphStore.C:524
    frame #5: 0x0000000100201932 dReal`dreal::nra_solver::slackTerm(this=0x0000000100d03fb0, e=0x0000000100d03d40, level=1, vs=0x0000000100d07b10 size=3) + 450 at nra_solver.cpp:624
    frame #6: 0x00000001001f0f27 dReal`dreal::nra_solver::slackAtom(this=0x0000000100d03fb0, e=0x0000000100d03ec0, level=1, lits=size=0) + 983 at nra_solver.cpp:671
    frame #7: 0x00000001001f09a2 dReal`dreal::nra_solver::inform(this=0x0000000100d03fb0, e=0x0000000100d03ec0) + 386 at nra_solver.cpp:101
    frame #8: 0x00000001000875c8 dReal`Egraph::inform(this=0x0000000102808200, e=0x0000000100d03ec0) + 1320 at EgraphSolver.C:81
    frame #9: 0x00000001001d0b1a dReal`THandler::enodeToVar(this=0x0000000100e04cf0, atm=0x0000000100d03ec0) + 618 at THandler.C:55
    frame #10: 0x00000001001d21de dReal`THandler::enodeToLit(this=0x0000000100e04cf0, elit=0x0000000100d03ec0) + 222 at THandler.C:137
    frame #11: 0x000000010011a1da dReal`SimpSMTSolver::addSMTClause(this=0x0000000102808800, smt_clause=size=1, in=0) + 730 at SimpSMTSolver.C:545
    frame #12: 0x0000000100061997 dReal`Cnfizer::giveToSolver(this=0x0000000100e01500, f=0x0000000100d03ec0) + 791 at Cnfizer.C:454
    frame #13: 0x0000000100061123 dReal`Cnfizer::cnfizeAndGiveToSolver(this=0x0000000100e01500, formula=0x0000000100d04830) + 707 at Cnfizer.C:70
    frame #14: 0x0000000100055348 dReal`OpenSMTContext::CheckSAT(this=0x00007fff5fbfedc8) + 472 at OpenSMTContext.C:735
    frame #15: 0x000000010005496a dReal`OpenSMTContext::executeIncremental(this=0x00007fff5fbfedc8) + 1098 at OpenSMTContext.C:272
    frame #16: 0x00000001000542b3 dReal`OpenSMTContext::executeCommands(this=0x00007fff5fbfedc8) + 179 at OpenSMTContext.C:212
    frame #17: 0x00000001000023dd dReal`main(argc=4, argv=0x00007fff5fbff280) + 3773 at main.cpp:120
    frame #18: 0x00007fff9234e5ad libdyld.dylib`start + 1
soonhokong commented 8 years ago

Closed by 2ef25c7