Example where the trick for checking a forall with no triggers does not work

Question

Example 2: This example is a simplication of a more complicated program where triggers cannot be generated

It seems like variable test1 is undefined, but if you assert the if-and-only-if postcondición of the method call, it is perfectly verified, however it seems that the truth value of test1 is unknown.

Please, could someone tell me what is wrong here, but not in the first example?

The problem could not be triggers, but I cannot guess where is. Indeed the first example was created to check if triggers absence could generate the problem

Thanks in advance.

datatype AExp = N(int)
                | NVar(name:string, nMin:int, nMax:int)
                | Plus(ae0:AExp, ae1:AExp)
 
datatype BExp = Asig(ae0: AExp, ae1: AExp) 

predicate wellDefinedAExp(ae: AExp, m: map<string,int>)
{
match ae
case N(n) => true
case NVar(name, min, max) => name in m 
case Plus(ae0, ae1) => wellDefinedAExp(ae.ae0, m) && wellDefinedAExp(ae.ae1, m)
}

function evalAExp(ae: AExp, m: map<string,int>): int
requires wellDefinedAExp(ae,m)
decreases ae
{
match ae
case N(n) => n
case NVar(name,_,_) => m[name]
case Plus(ae0, ae1) => evalAExp(ae0,m) + evalAExp(ae1,m)
}

predicate wellDefinedGRequirement(post:BExp, m: map<string,int>)
{ 
m != map[] &&
post.ae0.NVar? && 
wellDefinedAExp(post.ae0, m) && 
wellDefinedAExp(post.ae1, m) 
&&
(post.ae0.nMin <= evalAExp(post.ae1, m) <= post.ae0.nMax)
}

function transition(post:BExp, m: map<string,int>): map<string,int>
ensures wellDefinedGRequirement(post, m) <==> |transition(post,m)| > 0
{
if wellDefinedGRequirement(post, m) then
    m[post.ae0.name:= evalAExp(post.ae1,m)]    
else map[]
}

predicate wellDefinedSeq (seqR: seq<BExp>, m: map<string,int>)
{
|seqR|>0 &&
wellDefinedGRequirement(seqR[0],m) &&
forall j :: 2 <= j <= |seqR| 
            ==> wellDefinedGRequirement(seqR[j-1],i_transitions(j-1,seqR,m))       
}

function i_transitions(i:nat,seqR: seq<BExp>,m: map<string,int>): map<string,int>
requires 1 <= i <= |seqR|
{
if m == map[] then map[]
else if i == 1 then transition(seqR[0],m)
else transition(seqR[i-1], i_transitions(i-1,seqR,m))     
}

method wellDefinedSeqCheck (seqR:seq<BExp>,m:map<string,int>) returns (test:bool)
requires |seqR| > 0
ensures test <==> wellDefinedSeq(seqR,m)
{
if !wellDefinedGRequirement(seqR[0],m) {test:=false;}
else { var i := 2; 
       test := true;
       while i <= |seqR| && wellDefinedGRequirement(seqR[i-1],i_transitions(i-1,seqR,m))
            invariant 2 <= i <= |seqR|+1  
            invariant test <==> forall j :: 2 <= j < i ==> wellDefinedGRequirement(seqR[j-1],i_transitions(j-1,seqR,m))
            {
            i := i+1;
            }
       if i < |seqR|+1 {test := false;}
}}

method Main() {
var out1 := NVar("out1", 0, 100);
var out2:= NVar("out2", 0, 50);
var R0 := Asig(out1, N(10));
var R1 := Asig(out1, N(5));
var R2 := Asig(out2, Plus(out2, N(5)));
var  RSeq:= [R0, R1, R2, R2, R2];
var envir:= map[out1.name:= 30, out2.name:= 20];

var test1 := wellDefinedSeqCheck(RSeq,envir);
//assert test1; //This is not verified
//assert !test1; //Neither this
}