Quantified Bit Vectors - Error

10 views

Skip to first unread message

lykur...@gmail.com

unread,

May 7, 2020, 5:27:08 AM5/7/20

to Boolector

Hello everyone,

Recently I tried to use Boolector with quantifiers. Unfortunately I encountered a problem (I assume this is related to the quantifier usage, as this has never been an issue in the quantifier free case).

The problem is that Boolector reports:

[btor>main] CAUGHT SIGNAL 11
unknown
Segmentation fault

This was caused both by Boolector version 3.1.0 and 3.2.0, used with default options.

An example that causes this output, can be found in the attachment.

What causes this output - did I apply Boolector in a wrong way?

Thanks in advance

Example.smt2

Mathias Preiner

unread,

May 8, 2020, 1:31:54 PM5/8/20

to bool...@googlegroups.com

Thanks for the report! Looks like a problem with quantifiers in
(define-fun ...). We are looking into this.

Cheers,
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 view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/58e7262f-47ae-4db6-8cdd-49682d18f759%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/58e7262f-47ae-4db6-8cdd-49682d18f759%40googlegroups.com?utm_medium=email&utm_source=footer>.