Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005602OCaml~DO NOT USE (was: OCaml general)public2012-04-25 15:092015-12-11 19:04
Assigned To 
StatusclosedResolutionno change required 
PlatformlinuxOSubuntuOS Version10.10
Product Version3.12.1 
Target VersionFixed in Version 
Summary0005602: Adding a print changes the output of a function
DescriptionOn a modified version of the alt-ergo prover, adding a print (line 266 of file 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 line 490).
Steps To ReproduceDownload alt-ergo 0.94 on [^]
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
Compile: make
Run: alt-ergo.opt -theory axioms.why list-axiom-tests.why 2>&1 2> toto
Should return "Valid"
TagsNo tags attached.
Attached Filesgz file icon reproducer.tar.gz [^] (22,401 bytes) 2012-04-25 15:09

- Relationships

-  Notes
claire.dross (reporter)
2012-04-27 11:31

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
doligez (administrator)
2012-05-02 16:25

As you noted yourself, this is expected behaviour.

- Issue History
Date Modified Username Field Change
2012-04-25 15:09 claire.dross New Issue
2012-04-25 15:09 claire.dross File Added: reproducer.tar.gz
2012-04-27 11:31 claire.dross Note Added: 0007393
2012-05-02 16:25 doligez Note Added: 0007397
2012-05-02 16:25 doligez Status new => resolved
2012-05-02 16:25 doligez Resolution open => no change required
2015-12-11 19:04 xleroy Status resolved => closed
2017-02-23 16:36 doligez Category OCaml general => -OCaml general
2017-03-03 17:55 doligez Category -OCaml general => -(deprecated) general
2017-03-03 18:01 doligez Category -(deprecated) general => ~deprecated (was: OCaml general)
2017-03-06 17:04 doligez Category ~deprecated (was: OCaml general) => ~DO NOT USE (was: OCaml general)

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker