| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
| |
|
|
| |
mistake.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As it stands, Boogie abruptly aborts the prover by calling Kill() on the
associated process after receiving responses to all of its queries. In
most cases this is fine, but in general this is pretty bad: it yields to
all sorts of output corruption when user-supplied options require z3 to
write output to an auxiliary file (say, using /z3opt:TRACE=true). This
explains why VCC's Axiom Profiler often complains about a missing [eof]
after running Boogie with /z3opt:TRACE=true.
This patch fixes it by only falling back to Kill if the process seems to
have become unresponsive. That is, it starts by cleanly closing the
process input, which signals the end of the interactive session. It then
waits for a clean exit for 2s, and only after that does it resort to
calling Kill(). I've striven for minimal modifications to the logic, so
the patch still universally swallows errors that might occur while
closing the underlying stream, and still calls Kill() (I wouldn't be
against Boogie just hanging if z3 hangs too).
On my tests, z3 exits cleanly pretty much instantly after input is closed
anyway, so I don't expect the timeout to fire often (which would be one
more reason to actually remove that timeout, and condition Boogie's exit
on that of z3 IMO).
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
variable that begins with a ``.``. This was't an issue for Z3 which
ignores this but CVC4 is stricter and will emit an error
|
| | |
|
| |
|
|
|
|
|
|
|
| |
otherwise if either of the following happens
* if the solver hangs and we do CTRL+C
* if Boogie crashes
then some lines will be missing from the log.
|
| |
|
|
|
|
| |
where setting produce-unsat-cores to true has no effect unless the option is set last.
This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2
|
| | |
|
| |
|
|
|
| |
taken from ``bv_decl_plugin::get_op_names(...)`` in
``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code.
|
| |
|
|
|
|
|
| |
taken
from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp``
in the Z3 4.3.2 source code.
|
| |
|
|
|
| |
from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp``
from the Z3 4.3.2 source code.
|
| |
|
|
| |
when generating the VC.
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Fix some of the interfacing with Z3 4.3.2 in SMTLib. In particular:
* It makes the useSmtOutputFormat usable
* It fixes parsing of bit vectors that occur in the models returned by Z3
Similar stuff might be broken in the other interfaces to Z3, but it shouldn’t
be more broken than it already was.
|
| | |
| |
| |
| | |
Fix interfacing with CVC4 1.5
|
| | |
| |
| |
| | |
An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
|
| | | |
|
| | | |
|
| |/| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Patch by Jeroen Ketema
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The Model parser for SMT models is broken beyond repair
and this by-passes this. The code could be moved to the
model parser, but that's a refactoring for another day.
Also, the existing version already had multiple reparses
going on and this at least removes one of those.
Patch by Jeroen Ketema.
|
| | | | |
|
| |/ / |
|
| |/
|
|
|
|
| |
Only set produce-unsat-cores in the case /explainHoudini is passed. This
allows contract inference to be used with solvers that do no support unsat
cores, as long as no explanation of the Houdini run is required.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
There were many calls in the code to
``` new TokenTextWriter("<buffer>", buffer, false) ```
Prior to 61a94f409975 this was a call to the following constructor
```
TokenTextWriter(string filename, TextWriter writer, bool setTokens)
```
After that commit these then became calls to
```
TokenTextWriter(string filename, TextWriter writer, bool pretty)
```
An example of where this would cause issues was if ToString() was called on an
AbsyCmd then the its token would be modified because the setTokens parameter
was effectively set to True when the original intention was for it to be set
to false!
To fix this I've
* Removed the default parameter value for pretty and fixed all
uses so that we pass false where it was implicitly being set before
* Where the intention was to set setTokens to false this has been fixed so
it is actually set to false!
Unfortunately I couldn't find a way of observing this bug from the Boogie
executable so I couldn't create a test case. I could only observe it when I was
using Boogie's APIs.
|
| | |
|
Dan Liew
qadeer
akashlal
Ken McMillan
Valentin Wüstholz
U-REDMOND\kenmcmil
Clément Pit--Claudel
Akash Lal
akashlal