1 2 3 4 5 6 7 8
; COMMAND-LINE: --produce-abducts ; EXPECT: none (set-logic UFLRA) (declare-sort S0 0) (declare-fun S0-0 () S0) (declare-fun S0-1 () S0) (declare-fun v87 () Bool) (get-abduct A (and false (exists ((q117 S0)) (or v87 (and (= S0-1 q117) (= q117 S0-0))))))