SMT not using hypothesis

[henriquejosefaria]

Example:

require import AllCore StdOrder.
from Jasmin require import JModel JWord.

lemma xxx (x: W64.t):
 W64.to_uint x < W64.modulus => W64.to_uint x < W64.modulus.
proof.
  move => H. smt().

why3 Configuration

Executing: why3 config detect -C /Users/henriquefaria/.config/easycrypt/why3.conf
warning: cannot read config file /Users/henriquefaria/.config/easycrypt/why3.conf:
  /Users/henriquefaria/.config/easycrypt/why3.conf: No such file or directory
Found prover Alt-Ergo version 2.4.3, OK.
Found prover Alt-Ergo version 2.4.3 (alternative: FPA)
Found prover CVC5 version 1.0.9 (alternative: strings+counterexamples)
Found prover CVC5 version 1.0.9 (alternative: strings)
Found prover CVC5 version 1.0.9 (alternative: counterexamples)
Found prover CVC5 version 1.0.9, OK.
Found prover CVC4 version 1.8 (alternative: strings+counterexamples)
Found prover CVC4 version 1.8 (alternative: strings)
Found prover CVC4 version 1.8 (alternative: counterexamples)
Found prover CVC4 version 1.8, OK.
Found prover Z3 version 4.12.6 (alternative: counterexamples)
Found prover Z3 version 4.12.6, OK.
Found prover Z3 version 4.12.6 (alternative: noBV)
13 prover(s) added
Save config to /Users/henriquefaria/.config/easycrypt/why3.conf

[fdupress]

Simply the presence of the Jasmin eclib things in a require is enough to cause a trivial smt call to fail.

require import AllCore.
from Jasmin require JWord.

lemma xxx (x: int):
 x < 2^64 => x < 2^64.
proof.
  move => H. smt().

Removing the from Jasmin ... line allows the run to succeed.