User !=

using SymbolicFlashLoanReceiver as flashLoanReceiver

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

What does user != mean?

From Tutorials → lesson 09 → SymbolicPoolDemo → highLevel.spec


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 is a call to the public getter of the to var in flashLoanReceiver.

hope i answered your question.