[Quant] Add a tests for E-matching

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)))

src_colibri2/tests/solve/smt_quant/unsat/forall7.smt2

+(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)