Sources of nondeterminism in Prusti

[enjhnsn2]

Hello, I am getting nondeterministic failures when verifying a relatively small function (passes ~1/4 of the time), even when all timeout parameters are set to 0 (no timeout). Specifically the error I am getting is:

error: [Prusti internal error] Prusti encountered an unexpected internal error
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [inhale.failed:insufficient.permission; 0] Inhale might fail. There might be insufficient permission to access _1.val_ref.f$memlen (@0.0)

And the contents of my Prusti.toml:

counterexample = false
check_overflows = false
assert_timeout = 0
extra_verifier_args = [ "--checkTimeout=0", "--qpSplitTimeout=0", "--z3SaturationTimeout=0", "--numberOfParallelVerifiers=1" ]
enable_cache=true
dump_debug_info=true

I have two questions:

1. Are there any other timeout parameters / sources of nondeterminism that I don't account for as a part of my Prusti.toml I should know about? I think I've accounted for all of them, but the extra_verifier_args are undocumented, so I'm not 100% sure.
2. Any tips on debugging this issue? Places to look in the code, specific debugging steps (maybe run Z3 directly on the resulting query or something?), or any other tips would be greatly appreciated.

P.S. I'm trying to minimize a good code example that shows this behavior, but the code I'm having trouble with references a lot of structs/predicates defined as a part of a larger project, so its a little difficult. I'll post a code example if I find a good one.

[fpoli]

Could you check if the Viper dumps of Prusti (dump_viper_program=true) are deterministic?

The extra_verifier_args are defined here. I'm not familiar with all of them, but you can at least check the description. Be aware that via the extra_verifier_args it's also possible to set Z3 parameters. In single-threaded mode, however, Z3 should be deterministic.

[JonasAlaif]

@enjhnsn2 An easy way to check if the viper program is deterministically encoded is to use the PRINT_HASH flag and compare the hashes you get. Alternatively, if you want a diff of what changes between the Viper files, you could modify the two files here to both contain your small function and run the corresponding test in the parent directory. If you could post the function you're running into issues here, I'd be happy to add it to those tests to prevent a regression.