User != flashLoanReceiver.to(e)

CVL Support
1 
using SymbolicFlashLoanReceiver as flashLoanReceiver

rule user_solvency_on_flashLoan(address user) {
	env e;
	
	require user != currentContract && user != flashLoanReceiver.to(e) && user != flashLoanReceiver;

What does user != flashLoanReceiver.to(e) mean?

From Tutorials → lesson 09 → SymbolicPoolDemo → highLevel.spec
Link

Thanks

2

If you’ll look at the top of the spec file, you will find a using statement with flashLoanReceiver.
The using statement basically gives a name to an object of the specified contract (in this case SymbolicFlashLoanReceiver).

If you’ll go to the contract implemented in SymbolicFlashLoanReceiver.sol (Link) you’ll see that there is a public var called to.
The flashLoanReceiver is a dummy contract that act as the wallet/contract that receive the flash loan. The call flashLoanReceiver.to(e) is a call to the public getter of the to var in flashLoanReceiver.

hope i answered your question.