Segfault in OpenSMT

18 views

Skip to first unread message

Nicolas Bonifas

unread,

Feb 14, 2012, 6:12:16 AM2/14/12

to ope...@googlegroups.com

Hello,

OpenSMT (SVN r62) segfaults on the following short example:

(set-logic QF_IDL)
(set-info :smt-lib-version 2.0)
(declare-fun n () Int)
(assert (= n 42))
(check-sat)
(exit)

Here is a backtrace:

#0 TopLevelProp::arithmeticElimination (this=0xbffff198, top_level_arith=...,
substitutions=...) at TopLevelProp.C:373
#1 0x080b5313 in retrieveSubstitutions (substitutions=<optimized out>,
formula=0x81150a8, this=<optimized out>) at TopLevelProp.C:343
#2 TopLevelProp::doit (this=0xbffff198, formula=0x81150a8)
at TopLevelProp.C:81
#3 0x080941d7 in OpenSMTContext::staticCheckSAT (this=0xbffff238)
at OpenSMTContext.C:391
#4 0x080949a0 in OpenSMTContext::executeStatic (this=0xbffff238)
at OpenSMTContext.C:305
#5 0x0804b572 in main (argc=1, argv=0xbffff334) at src/bin/Main.C:169

Bests,
Nicolas

Roberto Bruttomesso

unread,

Feb 14, 2012, 8:14:52 AM2/14/12

to ope...@googlegroups.com

I've fixed it, thanks

Roberto

> --
> You received this message because you are subscribed to the Google Groups "opensmt" group.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to opensmt+u...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/opensmt?hl=en.
>