Solving with C API takes long while solving with the command line tool finishes instantly

[mariu...@fau.de]

Hi,

when I compile and execute the attached file (linked with Boolector 2.4.1), solving takes a very long time (it hits my 300 s timeout). However, when I dump the formula in btor or smt2 format before the call to boolector_sat and use this as input to the Boolector command line tool, it instantly reports "sat".

What is the reason for this odd behavior? Am I using the API in a wrong way?

Thank you in advance!

Marius

[Mathias Preiner]

Hi Marius,

You found a bug in the dumper of Boolector ;-) The formula that is
dumped is missing one constraint (50 root 1 39). This happens with
rewrite levels > 1.

Thanks for reporting this! This will be fixed in the upcoming release of
Boolector (due in the next 2-3 weeks).

Best,
Mathias

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To post to this group, send email to bool...@googlegroups.com
> <mailto:bool...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/boolector.
> For more options, visit https://groups.google.com/d/optout.