goals_limit := 1; Unify.search_bound := 40; Unify.trace_bound := 40; add_path "J"; add_path "JVM"; add_path "BV"; use_thy "Digest";