diff --git a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
index f8eacd78c9772e53e1b47c6e450dc50ac4b04301..a7adeeacbf66b7cd93319d2d2986eb7316c2b1b5 100644
--- a/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_quant/unsat/dune.inc
@@ -15,3 +15,5 @@
 (rule (alias runtest) (action (diff oracle forall5.smt2.res)))
 (rule (action (with-stdout-to forall6.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:forall6.smt2}))))
 (rule (alias runtest) (action (diff oracle forall6.smt2.res)))
+(rule (action (with-stdout-to forall7.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:forall7.smt2}))))
+(rule (alias runtest) (action (diff oracle forall7.smt2.res)))
diff --git a/src_colibri2/tests/solve/smt_quant/unsat/forall7.smt2 b/src_colibri2/tests/solve/smt_quant/unsat/forall7.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..eb89c1dd3770ec5bb350f5de1ea66e007d6ad5b3
--- /dev/null
+++ b/src_colibri2/tests/solve/smt_quant/unsat/forall7.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+
+(declare-sort S 0)
+(declare-fun a () S)
+(declare-fun P (S) Bool)
+(declare-fun f (S S) S)
+(declare-fun g (S) S)
+
+(assert (forall ((x S)) (= (f x x) (g x))))
+(assert (forall ((x S)) (P (g x))))
+
+(assert (not (P (f a a))))
+
+(check-sat)