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, caught signal 11 #91

Closed wintered closed 4 years ago

wintered commented 4 years ago 
[540] % z3 small.smt2
unsat
[541] % cvc4 -q small.smt2
unsat
[542] % boolector small.smt2
[btor>main] CAUGHT SIGNAL 11
unknown
Segmentation fault
[543] % 
[543] % cat small.smt2
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(assert (= a b (_ bv0 2)))
(assert (forall ((c (_ BitVec 2))) (distinct (bvudiv a c) b)))
(check-sat)
[544] %

OS: Ubuntu 18.04 Commit: ee44ed2