search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Segmentation fault [btor>main] CAUGHT SIGNAL 11 #94

Closed muchang closed 4 years ago

muchang commented 4 years ago

Hi, boolector throws out a segmentation fault on this case:

[505] % z3 small.smt2
sat
[506] % cvc4 -q small.smt2
unknown
[507] % boolector small.smt2
[btor>main] CAUGHT SIGNAL 11
unknown
Segmentation fault
[508] % 
[508] % cat small.smt2
(declare-fun f ((_ BitVec 1)) (_ BitVec 1))
(declare-fun g ((_ BitVec 1)) Bool)
(declare-fun h ((_ BitVec 1)) Bool)
(declare-const a (_ BitVec 1))
(assert (forall ((x (_ BitVec 1))) (distinct (= (f x) a) (xor (g x) (h x)))))
(check-sat)
[509] %

OS: Ubuntu 18.04 Commit: 0d478fe