search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.26k stars 1.48k forks source link

Segmentation fault while checking satisfiability using ocaml bindings #6071

Closed ntbertram closed 2 years ago

ntbertram commented 2 years ago

When checking for satisfiability for the following formula using the ocaml interface, I receive a segmentation fault.

(declare-datatypes ((tup_bool_bool 0)) (((tup_bool_bool (|1| Bool) (|2| Bool)))))
(declare-datatypes ((tup_tup_bool_bool_bool 0)) (((tup_tup_bool_bool_bool (|1| tup_bool_bool) (|2| Bool)))))
(declare-fun ret () tup_tup_bool_bool_bool)
(assert (forall ((ret1 tup_tup_bool_bool_bool))
  (let ((a!1 (forall ((ret2 tup_bool_bool) (ret1!1 Bool))
               (let ((a!1 (forall ((ret2!1 Bool) (ret1!2 Bool))
                            (or (not (and ret2!1 (not ret1!2)))
                                (= ret2 (tup_bool_bool ret2!1 ret1!2))))))
                 (or (not (and a!1 (not ret1!1)))
                     (= ret1 (tup_tup_bool_bool_bool ret2 ret1!1))))))
        (a!2 (forall ((ret2 tup_bool_bool) (ret1!1 Bool))
               (let ((a!1 (forall ((ret1!2 tup_tup_bool_bool_bool))
                            (or (not (= ret1!2 ret1)) (= ret2 (|1| ret1!2)))))
                     (a!2 (forall ((ret1!2 tup_tup_bool_bool_bool))
                            (or (not (= ret1!2 ret1)) (= ret1!1 (|2| ret1!2))))))
                 (or (not (and a!1 a!2))
                     (= ret (tup_tup_bool_bool_bool ret2 ret1!1)))))))
    (or (not a!1) a!2))))

However, if I take the solver in ocaml and output it as a string (in SMT-lib format) and give it to Z3 directly on my computer, it gives sat. I am using the latest version of Z3 for ocaml (4.8.14) and on my computer I am using Z3 version 4.8.18. I have tried this both on a machine running linux, and a machine running mac os. I can give more information if needed, though it may be a pain to build this formula by hand using the ocaml bindings.

NikolajBjorner commented 2 years ago

There isn't adequate information (such as a self-contained repro) to be able to give useful feedback on this report. Given that z3 is open source you may be able to also debug this directly.