Skip to content

GitLab

Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Closed
Created by DAILLER Sylvain@sdaillerDeveloper

Removing Inline_trivial

Hello,

I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes cvc4 1.5 fail on some files (bench/ce/array_mono.mlw).

Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information