Hints are not filtered by using_facts_from

[mtzguido]

cc @nikswamy , this may be related to the weirdness you noticed with context pruning?

This file is in bug-reports as a negative test, we should fail to prove this without any facts (-*)

module Bug1614a

assume val x : (y:int{y==1})

(* An abbreviation for triggering the query *)
let f () : Pure unit (requires (x + 1 == 2)) (ensures (fun () -> True)) = ()

#set-options "--using_facts_from '-*'"

[@@expect_failure [19]]
let _ = f ()

$ ./bin/fstar.exe Bug1614a.fst --query_stats
Refreshing the z3proc (ask_count=0 old=[cmd= args=[]] new=[cmd=z3-4.8.5 args=[-smt2, -in, smt.random_seed=0]])
(Bug1614a.fst(6,74-6,76))       Query-stats (Bug1614a.f, 1)     succeeded in 191 milliseconds with fuel 2 and ifuel 1 and rlimit 5
Refreshing the z3proc (ask_count=1 old=[cmd=z3-4.8.5 args=[-smt2, -in, smt.random_seed=0]] new=[cmd=z3-4.8.5 args=[-smt2, -in, smt.random_seed=0]])
(Bug1614a.fst(11,0-11,12))  Query-stats (Bug1614a.uu___0, 1)        failed {reason-unknown=unknown because (incomplete quantifiers)} in 15 milliseconds with fuel 2 and ifuel 1 and rlimit 5
(Bug1614a.fst(11,0-11,12))      Query-stats (Bug1614a.uu___0, 1)        failed {reason-unknown=unknown because (incomplete quantifiers)} in 0 milliseconds with fuel 2 and ifuel 2 and rlimit 5
(Bug1614a.fst(11,0-11,12))      Query-stats (Bug1614a.uu___0, 1)        failed {reason-unknown=unknown because (incomplete quantifiers)} in 0 milliseconds with fuel 4 and ifuel 2 and rlimit 5
(Bug1614a.fst(11,0-11,12))      Query-stats (Bug1614a.uu___0, 1)        failed {reason-unknown=unknown because (incomplete quantifiers)} in 0 milliseconds with fuel 8 and ifuel 2 and rlimit 5
* Warning 252 at Bug1614a.fst(11,8-11,9):
  - Assertion failed
  - See also Bug1614a.fst(6,31-6,43)

Verified module: Bug1614a
All verification conditions discharged successfully
TOTAL TIME 322 ms: ./bin/fstar.exe Bug1614a.fst --query_stats

That's good.

Now, if we use hints, with the file currently in the repo

$ ./bin/fstar.exe Bug1614a.fst --query_stats --use_hints
Refreshing the z3proc (ask_count=0 old=[cmd= args=[]] new=[cmd=z3-4.8.5 args=[-smt2, -in, smt.random_seed=0]])
(/home/guido/r/fstar/master/Bug1614a.fst) digest is invalid; using potentially stale hints from /home/guido/r/fstar/master/Bug1614a.fst.hints.
(Bug1614a.fst(6,74-6,76))       Query-stats (Bug1614a.f, 1)     succeeded (with hint) in 8 milliseconds with fuel 2 and ifuel 1 and rlimit 5
(Bug1614a.fst(11,0-11,12))      Query-stats (Bug1614a.uu___0, 1)        succeeded (with hint) in 9 milliseconds with fuel 2 and ifuel 1 and rlimit 5
* Error 303 at Bug1614a.fst(11,0-11,12):
  - This top-level definition was expected to fail, but it succeeded

Verified module: Bug1614a
1 error was reported (see above)

The query succeeds when it should not. Attaching the hints here. Bug1614a.fst.hints.txt