From c1bdbc8078517ee52acd7c7357b999bab62175bf Mon Sep 17 00:00:00 2001 From: Philipp Ruemmer Date: Tue, 16 Jan 2018 14:48:52 +0100 Subject: [PATCH] updated answers to include correct types --- regression-tests/horn-adt/Answers | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/regression-tests/horn-adt/Answers b/regression-tests/horn-adt/Answers index fc83290c..04de31a9 100644 --- a/regression-tests/horn-adt/Answers +++ b/regression-tests/horn-adt/Answers @@ -2,12 +2,12 @@ simple-adt-horn.smt2 Theories: ADT(P) sat -(define-fun I1 ((A Int)) Bool (or (and (= (right A) true) (= (left A) 0)) (and (= (right A) true) (>= (left A) 2)))) -(define-fun I2 ((A Int)) Bool (and (not (= (right A) true)) (>= (left A) 1))) +(define-fun I1 ((A Pair)) Bool (or (and (= (right A) true) (= (left A) 0)) (and (= (right A) true) (>= (left A) 2)))) +(define-fun I2 ((A Pair)) Bool (and (not (= (right A) true)) (>= (left A) 1))) bool.smt2 sat -(define-fun Inv ((A Int) (B Int)) Bool (or (and (= A false) (= B false)) (and (= A true) (= B true)))) +(define-fun Inv ((A Bool) (B Bool)) Bool (or (and (= A false) (= B false)) (and (= A true) (= B true)))) bool-unsat.smt2 unsat @@ -19,7 +19,7 @@ unsat list-synasc.smt2 Theories: ADT(Nil, Cons) sat -(define-fun Concat ((A Int) (B Int) (C Int)) Bool (or (and (= B C) (and (= (_size A) 1) (= (* (- 1) (_size A)) (- 1)))) (and (= (+ (_size C) (- (* (- 1) (_size B)) (_size A))) (- 1)) (= (head C) (head A))))) +(define-fun Concat ((A IList) (B IList) (C IList)) Bool (or (and (= B C) (and (= (_size A) 1) (= (* (- 1) (_size A)) (- 1)))) (and (= (+ (_size C) (- (* (- 1) (_size B)) (_size A))) (- 1)) (= (head C) (head A))))) list-synasc-unsat.smt2 Theories: ADT(Nil, Cons)