Adding a print changes the output of a function #5602
Labels
Comments
|
Comment author: claire.dross The non-determinism is caused by a call of the garbage collector (triggered by the use of Format) that modifies the order of terms in a weak hash table. Thanks for your help |
|
Comment author: @damiendoligez As you noted yourself, this is expected behaviour. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Original bug ID: 5602
Reporter: claire.dross
Status: closed (set by @xavierleroy on 2015-12-11T18:04:32Z)
Resolution: not a bug
Priority: normal
Severity: minor
Platform: linux
OS: ubuntu
OS Version: 10.10
Version: 3.12.1
Category: ~DO NOT USE (was: OCaml general)
Monitored by: mehdi @Chris00
Bug description
On a modified version of the alt-ergo prover, adding a print (line 266 of file my_matching.ml) changes the ouput of the solver on a test file. With the print it finds that the formula is true and without it it fails because it reaches a limit in the number of splits allowed (see file cc.ml line 490).
Steps to reproduce
Download alt-ergo 0.94 on http://alt-ergo.lri.fr/
Apply the patch diff.patch,
Compile: ./configure, make (need ocamlgraph 1.81)
Run: alt-ergo.opt -theory axioms.why list-axiom-tests.why 2>&1 2> toto
Should return "I don't know"
Decomment line 266 of file my_matching.ml
Compile: make
Run: alt-ergo.opt -theory axioms.why list-axiom-tests.why 2>&1 2> toto
Should return "Valid"
File attachments
The text was updated successfully, but these errors were encountered: