a weird test-case

The entailment is resolved differently whether it's run by logic_test or
by symb_test. The logic in both cases is a single rule:

rule toto:
 | |- f(?x,?y) = numeric_const("1")
without |- ?x = ?y
if
 | |- ?x = ?y

Trying to prove the entailment f(?x,?y) = numeric_const("1") |-
directly gives (prover_tests/weird.out):

Goal  | numeric_const("1")=f(x, y) |-
-|

Start time :0.000000
> | numeric_const("1")=f(x, y) |-  -|

.Done.

However, if checked as pre |- post during symbolic execution, I get
(symb_tests/weird.out):

Goal  | numeric_const("1")=f(x, y) |-
-|

Start time :0.000000
> | numeric_const("1")=f(x, y) |-  -|

Match rule toto
-> | numeric_const("1")=f(x, y) |- x=y -|

--> | numeric_const("1")="1" * numeric_const("1")=f(x, y) |- x=y -|

ERROR: Cannot prove postcondition.
!Needed to prove:
   | numeric_const("1")="1" * numeric_const("1")=f(x, y) |- x=y -|