"fd:6: hGetLine: end of file" in Cryptol

Question

我已经从源代码编译并安装了cvc4。Cvc4 是按照建议下载并安装的，Cryptol 是从它的 git 存储库下载的。沙盒和安装完成，没有错误（GHC 7.8.3 x86_64）。只有在调用 cryptol 并发出 :prove True 后，才会出现此问题。这是一切：

athan@namek ~/lib> cryptol
                        _        _
   ___ _ __ _   _ _ __ | |_ ___ | |
  / __| '__| | | | '_ | __/ _ | |
 | (__| |  | |_| | |_) | || (_) | |
  ___|_|   __, | .__/ _____/|_|
            |___/|_| version 2.1.0 (8898348)
Loading module Cryptol
Cryptol> :prove True
cryptol: fd:6: hGetLine: end of file
athan@namek ~/lib> 

对此的任何帮助都将是巨大的。对我来说，感觉就像找不到一个共享库。这会导致此问题吗？谢谢。

Answer 1

在评论中总结对话：

问题中提到的"文件结束"错误通常归因于感兴趣的证明者（在本例中为 CVC4）仅"部分安装" - 在我的情况下，这始终是共享库的问题，可以通过从命令行调用二进制文件（cvc、布尔值等）来发现。 REPL将终止的错误票证位于Cryptol的github上。 幸运的是，这个问题在上游SBV中得到了修复，很快就会出现在Cryptol的SBV分支中。

WRT AthanClark的特殊情况仍然不知道CVC4在被Cryptol调用时失败的原因和方式 - 可能性包括cryptol调用与我们预期的二进制文件不同的二进制文件或环境差异，例如LD_LIBARARY路径变量。 无论哪种方式，听起来他都能够成功地使用替代证明者（boolector）。

编辑：如果你能产生Athan的错误，CVC在SBV之外而不是在SBV内部工作......你住在波特兰，然后给我发一条消息，出现在我的办公室，告诉我，我会感兴趣的。