0005602: Adding a print changes the output of a function

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005602

OCaml

OCaml general

public

2012-04-25 15:09

2012-05-02 16:25

Reporter

claire.dross

Assigned To

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

no change required

Platform

linux

ubuntu

OS Version

10.10

Product Version

3.12.1

Target Version

Fixed in Version

Summary

0005602: Adding a print changes the output of a function

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"

Tags

No tags attached.

Attached Files

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 (manager) 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