horn segmentation fault and assertion violation at ../src/muz/rel/aig_exporter.cpp Line: 272 #3003
Description
Hi,
For this formula:
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= f g))
(check-sat-using horn)
Z3 (debug mode) throws out an assertion violation and Z3 (release mode) throws out a segmentation fault:
[576] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/muz/rel/aig_exporter.cpp
Line: 272
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[577] % z3release small.smt2
Segmentation fault
OS: Ubuntu 18.04
Commit: 85fd139