l <- llvm_load_module "double.bc";
double_imp <- crucible_llvm_extract l "double_imp";
double_ref <- crucible_llvm_extract l "double_ref";
let thm = {{ \x -> double_ref x == double_imp x }};

let picosat = external_cnf_solver "picosat" ["%f"];
r <- prove picosat thm;
print r;
print "Done.";
