Translation from DSEML to SMT crashes as it encounters the same expression twice
As the DSMLtoSMTTransformator
stores constraints and objectives in the
translatedExpressions
after processing them, the HashBiMap
throws an
value already present
error if two identical expressions are found
within one DSE run - even if they are part of distinct rule sets.
Expected behavior
Constraints and objectives should be idempotent - adding them once or multiple times should not change the result of the exploration.
How to reproduce
After importing the attaches project into the DSE view, one can execute a deployment synthesis selecting the existing constraint set.
(from redmine: issue id 3771, created on 2019-07-12, closed on 2019-07-25)
- Uploads:
- dse_project.af3_23 Minimal AF3 project for testing