conjunctions in assertion causing violated invariants

[polgreen]

This works:

__CPROVER_bool EXPRESSION(int, int);
int nondet_int();

void main()
{
 int a=nondet_int();
 int b=nondet_int();
 int c=nondet_int();

__CPROVER_assert(EXPRESSION(a,b)==(a>b),"");
__CPROVER_assert(EXPRESSION(b,a)==(b>a),"");
}

This doesn't:

__CPROVER_bool EXPRESSION(int, int);
int nondet_int();

void main()
{
 int a=nondet_int();
 int b=nondet_int();
 int c=nondet_int();

__CPROVER_assert(EXPRESSION(a,b)==(a>b) && EXPRESSION(b,a)==(b>a),"");
}

Invariant violation:

Invariant check failed
File: goto_state.cpp:149 function: apply_condition
Condition: false
Reason: Unreachable