Merge branch 'adt' of https://github.com/uuverifiers/eldarica into adt

uuverifiers · Jan 17, 2018 · 1c827b1 · 1c827b1
2 parents c3fc421 + c1bdbc8
commit 1c827b1
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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)