1; COMMAND-LINE: --quant-ind --incremental --rewrite-divk 2(set-logic ALL_SUPPORTED) 3(declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) 4(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2)))) 5(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil)))) 6; EXPECT: unsat 7(push 1) 8(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0))))))) 9(check-sat) 10(pop 1) 11 12(assert (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0)))) 13 14; EXPECT: unsat 15(push 1) 16(assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0)))))))) 17(check-sat) 18(pop 1) 19 20(assert (forall (($l1$0 Lst) ($l2$0 Lst)) (= (rev (app $l1$0 $l2$0)) (app (rev $l2$0) (rev $l1$0))))) 21 22; EXPECT: unsat 23(push 1) 24(assert (not (=> true (and (forall (($l1$0 Lst)) (= (rev (rev $l1$0)) $l1$0)))))) 25(check-sat) 26(pop 1) 27 28 29