Adapt to changes from Eldarica

uuverifiers · Mar 20, 2024 · f33c6a3 · f33c6a3
1 parent 860ff13
commit f33c6a3
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 8 deletions.
diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala
@@ -30,23 +30,26 @@
 
 package tricera
 
+import java.io.{FileOutputStream, PrintStream}
+import java.nio.file.{Files, Paths}
+import sys.process._
+
 import ap.parser.IExpression.{ConstantTerm, Predicate}
 import ap.parser.{IAtom, IConstant, IFormula, VariableSubstVisitor}
+
 import hornconcurrency.ParametricEncoder
 
-import java.io.{FileOutputStream, PrintStream}
-import java.nio.file.{Files, Paths}
 import lazabs.horn.bottomup.HornClauses.Clause
-import tricera.concurrency.{CCReader, TriCeraPreprocessor}
+import lazabs.horn.Util.NullStream
 import lazabs.prover._
+
+import tricera.concurrency.{CCReader, TriCeraPreprocessor}
 import tricera.Util.SourceInfo
 import tricera.benchmarking.Benchmarking._
 import tricera.concurrency.CCReader.{CCAssertionClause, CCClause}
 import tricera.concurrency.ccreader.CCExceptions._
 import tricera.parsers.YAMLParser._
 
-import sys.process._
-
 ////////////////////////////////////////////////////////////////////////////////
 
 object Main {
@@ -256,7 +259,7 @@ class Main (args: Array[String]) {
  if (princess)
  Prover.setProver(lazabs.prover.TheoremProver.PRINCESS)
  val outStream =
- if (logStat) Console.err else lazabs.horn.bottomup.HornWrapper.NullStream
+ if (logStat) Console.err else NullStream
 
  Console.withOut(outStream) {
  println(

diff --git a/src/tricera/concurrency/ReaderMain.scala b/src/tricera/concurrency/ReaderMain.scala
@@ -31,7 +31,7 @@ package tricera.concurrency
 
 import ap.parser.{IBoolLit, ITerm, PrincessLineariser, IExpression}
 import IExpression.Predicate
-import lazabs.horn.bottomup.HornTranslator
+import lazabs.horn.HornTranslator
 import lazabs.horn.bottomup.HornClauses.Clause
 import lazabs.viewer.HornSMTPrinter
 import hornconcurrency.{ParametricEncoder, VerificationLoop}

diff --git a/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala b/src/tricera/concurrency/ccreader/CCBinaryExpressions.scala
@@ -63,7 +63,7 @@ object CCBinaryExpressions {
  throw new TranslationException(
  getLineString(lhs.srcInfo) +
  s"Could not apply binary operator: $this\n")
- case e => throw e
+ case e : Throwable => throw e
  }
  }