pushBacktrackPoint, popBacktrackPoint

[Florian Corzilius]

Hey again!

I've got another problem:

It appears after asserting several constraints and calling "check"
with result False. I fill the explanation vector with an infeasible
subset of the asserted constraints and OpenSMT calls
"popBacktrackPoint" several times. Afterwards OpenSMT calls
"pushBacktrackPoint" directly, which I didn't expect. Could you
explain to me why this happens?

Thanks,

Florian

[Roberto Bruttomesso]

Hi,

I am not sure I understand the question. It might be perfectly fine behaviour, it just means that the sat solver is trying another branch of exploration that is feasible from the Boolean perspective. Providing some printout might help us understanding more about it

Cheers

>
> Thanks,
>
> Florian
>
> --
> 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.
>

Roberto Bruttomesso, PhD -
http://tinyurl.com/r0b3r70

[Florian Corzilius]

Hi Roberto,

I found the problem. OpenSMT first pushes a backtrack point and then
asserts an enode resp. a constraint. I handle it vice versa.

Best regards,

Florian