Re: [isabelle] Error Building HOL-Word

Hello Mario.

It looks like z3 isn't working in your environment. There's a copy of z3 bundled with isabelle, which is meant to work on any given platform, but a colleague of mine has had it terminate like that when running on his Windows machine.

There was a patch we recommended a while back which replaces the two uses of "smt" in the standard Isabelle theories with other proof methods. I think that patch has now been accepted, but you might be using a version where you don't have it yet. You can probably hand apply it.

OK, found it. There was a discussion here in December, which you can see on the web here:

You could hand-edit the two theories I quoted to replace the proofs with the ones I mentioned in that email. It's a dirty solution, but it should get you going for now.

An alternative would be to try to figure out what's up with executing z3 in your system. I don't know so much about that.


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Mario Alvarez <mmalvare at>
Sent: Thursday, March 22, 2018 5:30 AM
To: isabelle-users at
Subject: [isabelle] Error Building HOL-Word

Hi Isabelle-Users,

I am trying to compile some files from the eth-isabelle
<> project using the command-line
version of Isabelle (e.g. isabelle process -T TheoryName). It seems like
the error is due to a dependency on the HOL-Word library.

In fact, I notice that the HOL-Word library fails to build. When I run
isabelle build HOL-Word, I get a failure with the following error (at the

### theory "HOL-Word.WordBitwise"
### 0.591s elapsed time, 2.297s cpu time, 0.234s GC time
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "apply" (line 284 of
*** Solver z3: Solver terminated abnormally with error code 110
*** At command "by" (line 12 of "~~/src/HOL/Word/Misc_Numeric.thy")
Unfinished session(s): HOL-Word
0:00:37 elapsed time, 0:01:11 cpu time, factor 1.91

I assume this isn't expected behavior for trying to build HOL-Word (but let
me know if I'm wrong about that).

Strangely, this doesn't appear to be a problem when I open the files that
require this dependency in the JEdit interface to Isabelle: the file
processes successfully without any errors. Do you have any ideas why this
might be failing and what I can do to get it to build?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.