You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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"
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.
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: