System.IO.IOException: Write fault on path ...[Unknown]

[gconnell]

Running on intel NUC:

Here's some info on the box, showing among other things that:

1. we have a binary
2. we can read/write the directory
3. we have space on the drive
4. we have >=v4 mono

gconnell@tinyduck:~/d1.9.7/dafny$ uname -a
Linux tinyduck 3.13.0-107-generic #154-Ubuntu SMP Mon Dec 19 19:20:26 UTC 2016 i686 i686 i686 GNU/Linux
gconnell@tinyduck:~/d1.9.7/dafny$ ls -l -d . Dafny.exe pax.dfy
drwxrwxr-x 3 gconnell gconnell  4096 Feb  5 21:59 .
-rwxrw-r-- 1 gconnell gconnell 20992 Apr  1  2016 Dafny.exe
-rw-rw-r-- 1 gconnell gconnell    82 Feb  5 21:51 pax.dfy
gconnell@tinyduck:~/d1.9.7/dafny$ df -h .
Filesystem      Size  Used Avail Use% Mounted on
/dev/dm-0       102G   70G   28G  72% /
gconnell@tinyduck:~/d1.9.7/dafny$ mono --version
Mono JIT compiler version 4.6.2 (Stable 4.6.2.16/ac9e222 Tue Jan  3 11:57:29 UTC 2017)
Copyright (C) 2002-2014 Novell, Inc, Xamarin Inc and Contributors. www.mono-project.com
    TLS:           __thread
    SIGSEGV:       altstack
    Notifications: epoll
    Architecture:  x86
    Disabled:      none
    Misc:          softdebug 
    LLVM:          supported, not enabled.
    GC:            sgen

Here's the program I'm trying to test:

gconnell@tinyduck:~/d1.9.7/dafny$ cat pax.dfy 
method x(a: int) returns (b: int)
  requires a > 0
  ensures b < a
{
  b := -a;
}

And here's the error I'm getting:

gconnell@tinyduck:~/d1.9.7/dafny$ mono Dafny.exe pax.dfy 
Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
[ERROR] FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.IO.IOException: Write fault on path /home/gconnell/d1.9.7/dafny/[Unknown]
  at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00086] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x000a5] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x00094] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000ee] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.TextWriter.WriteLine (System.String value) [0x00083] in <8f2c484307284b51944a1a13a14c0266>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00036] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001e] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Collections.Generic.IList`1[T] namedAssumeVars) [0x00025] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x00233] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00716] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
   --- End of inner exception stack trace ---
  at System.AggregateException.Handle (System.Func`2[T,TResult] predicate) [0x00076] in <8f2c484307284b51944a1a13a14c0266>:0 
  at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, System.String programId, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId) [0x004d4] in <feed6349d12c413ab062f6060c810f35>:0 
  at Microsoft.Dafny.DafnyDriver.BoogiePipelineWithRerun (Microsoft.Boogie.Program program, System.String bplFileName, Microsoft.Boogie.PipelineStatistics& stats, System.String programId) [0x0010e] in <54a86185970b494c820320fda4961323>:0 
  at Microsoft.Dafny.DafnyDriver.ProcessFiles (System.Collections.Generic.IList`1[T] dafnyFileNames, System.Collections.ObjectModel.ReadOnlyCollection`1[T] otherFileNames, Microsoft.Dafny.ErrorReporter reporter, System.Boolean lookForSnapshots, System.String programId) [0x003a3] in <54a86185970b494c820320fda4961323>:0 
  at Microsoft.Dafny.DafnyDriver.ThreadMain (System.String[] args) [0x002fb] in <54a86185970b494c820320fda4961323>:0 
  at Microsoft.Dafny.DafnyDriver+<>c__DisplayClass1.<Main>b__0 () [0x00001] in <54a86185970b494c820320fda4961323>:0 
  at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00017] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x0008d] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x00031] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.Threading.ThreadHelper.ThreadStart () [0x0000b] in <8f2c484307284b51944a1a13a14c0266>:0 
---> (Inner Exception #0) System.IO.IOException: Write fault on path /home/gconnell/d1.9.7/dafny/[Unknown]
  at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00086] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x000a5] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x00094] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000ee] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.TextWriter.WriteLine (System.String value) [0x00083] in <8f2c484307284b51944a1a13a14c0266>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00036] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001e] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Collections.Generic.IList`1[T] namedAssumeVars) [0x00025] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x00233] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00716] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 <---

---> (Inner Exception #1) System.IO.IOException: Write fault on path /home/gconnell/d1.9.7/dafny/[Unknown]
  at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00086] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x000a5] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x00094] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000ee] in <8f2c484307284b51944a1a13a14c0266>:0 
  at System.IO.TextWriter.WriteLine (System.String value) [0x00083] in <8f2c484307284b51944a1a13a14c0266>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00036] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001e] in <471f888247164f639caaf4ecc8194fa2>:0 
  at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Collections.Generic.IList`1[T] namedAssumeVars) [0x00025] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x00233] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 
  at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00716] in <df17c9efe6ac44a9b952cae68f38b1f6>:0 <---

Dafny was installed by unzipping the 1.9.7 binaries zip. Unzipping the 1.9.8 binaries zip does the same thing. Building from source also does the same thing.

It always includes path ...[Unknown]

I have no familiarity or experience with Mono or .NET, so sorry if this is a trivial fix. Happy to try anything if you're interested in debugging further.

[gconnell]

Interestingly, just ran this same thing on a non-NUC computer, and things worked fine.

gconnell@gameyduck:~/dafny$ uname -a
Linux gameyduck 4.4.0-31-generic #50-Ubuntu SMP Wed Jul 13 00:07:12 UTC 2016 x86_64 x86_64 x86_64 GNU/Linux

Going to close this for now, as it appears to be device-specific, but happy to run any additional tests if you'd like.

[cpitclaudel]

I think I remember running into this. Does it happen if you run the dafny wrapper (dafny) instead of mono Dafny.exe). Going by my own answer to http://stackoverflow.com/questions/15399234/cant-write-input-to-process-c-sharp-mono , this could be due to your z3 executable being a broken symlink.

[xiexiewww]

Have you solved this problem? I am encountering this,could you help me?

[cpitclaudel]

Did you try my suggestions above? Check whether your z3 is a broken link, an check whether running Dafny directly works.

[xiexiewww]

Thank you very much! I have solve it,with downing and installing z3 of linux-based distribution. I am runing dafny in linux system,but there is a z3.exe in my project! Interestingly!

[cpitclaudel]

Great.

[robin-aws]

Could this be reopened to address the fact that this should be a lot easier to diagnose? I've now hit this twice in a row for different reasons (the second time because I accidentally downloaded the wrong z3 distribution). It looks like it's just a matter of configuring the Boogie logger correctly so that you get a more helpful error.

[lavaleri]

I was also hit with this issue, for the same reason as @robin-aws above.

I accidentally downloaded the z3 distro for Linux when I needed the one for Mac. This seems to be a pretty easy mistake to make, so it would save a lot of time if the error message was more clear.