diff --git a/regression-tests/horn-adt/Answers b/regression-tests/horn-adt/Answers
index 2b014750..5a7e4d43 100644
--- a/regression-tests/horn-adt/Answers
+++ b/regression-tests/horn-adt/Answers
@@ -86,7 +86,7 @@ sat
 de-brujin-bug.smt2
 sat
 (define-fun mmin ((A f)) Bool (= (h 0 g) A))
-(define-fun n ((A f)) Bool (or (or (and (and (= (_size A) (_size g)) (= (_size e) 1)) (>= (_size g) 1)) (and (and (and (is-b e) (= (_size e) 3)) (and (>= (_size A) 1) (>= (_size g) 1))) (is-b e))) (and (and (and (is-b e) (and (and (and (and (or (and (is-g A) (>= (_size e) 4)) (and (is-h A) (>= (_size e) 5))) (or (and (is-g A) (>= (_size e) 5)) (and (is-h A) (>= (_size e) 4)))) (>= (+ (_size A) (_size e)) 6)) (>= (_size A) 1)) (>= (_size g) 1))) (is-b e)) (= (mod (+ 1 (_size e)) 2) 0))))
+(define-fun n ((A f)) Bool (= (_size A) 1))
 (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
 
 list-synasc-unsat.smt2
diff --git a/regression-tests/horn-arrays/Answers b/regression-tests/horn-arrays/Answers
index 3537665d..e9bbfd36 100644
--- a/regression-tests/horn-arrays/Answers
+++ b/regression-tests/horn-arrays/Answers
@@ -224,8 +224,8 @@ sat
 (define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
 (define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
 (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
-(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) B) (and (<= D 0) (and (= D 1) (= (select C 0) (select var0 0))))))) (= 1 A)))
-(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) C)) (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0)))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) C) (exists ((var1 (Array Int Int))) (and (= (store var1 D 1) B) (and (<= D 0) (and (= D 1) (= (select var0 0) (select var1 0))))))))) (= 1 A)))
+(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
+(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
 (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
 (define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
 (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))
@@ -294,8 +294,8 @@ sat
 (define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
 (define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
 (define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
-(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) B) (and (<= D 0) (and (= D 1) (= (select C 0) (select var0 0))))))) (= 1 A)))
-(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) C)) (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0)))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) C) (exists ((var1 (Array Int Int))) (and (= (store var1 D 1) B) (and (<= D 0) (and (= D 1) (= (select var0 0) (select var1 0))))))))) (= 1 A)))
+(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
+(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
 (define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
 (define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
 (define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))