Skip to content

Commit 5a943b0

Browse files
authored
Merge pull request #720 from viperproject/auto-update-submodules
Update Submodules
2 parents 88e0a9b + 495c9f6 commit 5a943b0

File tree

2 files changed

+7
-1
lines changed

2 files changed

+7
-1
lines changed

src/main/scala/viper/gobra/backend/ViperBackends.scala

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,9 @@ object ViperBackends {
4444
case MCE.OnDemand => "2"
4545
}
4646
options ++= Vector(s"--exhaleMode=$mceSiliconOpt")
47+
// Gobra seems to be much slower with the new silicon axiomatization of collections.
48+
// For now, we stick to the old one.
49+
options ++= Vector("--useOldAxiomatization")
4750
if (config.assumeInjectivityOnInhale) {
4851
options ++= Vector("--assumeInjectivityOnInhale")
4952
}
@@ -128,6 +131,9 @@ object ViperBackends {
128131
var options: Vector[String] = Vector.empty
129132
options ++= Vector("--logLevel", "ERROR")
130133
options ++= Vector("--disableCatchingExceptions")
134+
// Gobra seems to be much slower with the new silicon axiomatization of collections.
135+
// For now, we stick to the old one.
136+
options ++= Vector("--useOldAxiomatization")
131137
val mceSiliconOpt = config.mceMode match {
132138
case MCE.Disabled => "0"
133139
case MCE.Enabled => "1"

viperserver

0 commit comments

Comments
 (0)