Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005602OCamlOCaml generalpublic2012-04-25 15:092012-05-02 16:25
Reporterclaire.dross 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno 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 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 ReproduceDownload 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"
TagsNo tags attached.
Attached Filesgz file icon reproducer.tar.gz [^] (22,401 bytes) 2012-04-25 15:09

- Relationships

-  Notes
(0007393)
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
(0007397)
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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker