version 2.0.3

build.sbt

@@ -2,9 +2,9 @@
 lazy val commonSettings = Seq(
     name := "Eldarica",
     organization := "uuverifiers",
-    version := "2.0.2",
+    version := "2.0.3",
     scalaVersion := "2.11.12",
-    crossScalaVersions := Seq("2.11.12", "2.12.8"),
+    crossScalaVersions := Seq("2.11.12", "2.12.10"),
     fork in run := true,
     cancelable in Global := true,
     publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) )
@@ -124,7 +124,7 @@ lazy val root = (project in file(".")).
            "-language:implicitConversions,postfixOps,reflectiveCalls"),
     scalacOptions += (scalaVersion map { sv => sv match {
       case "2.11.12" => "-optimise"
-      case "2.12.8" => "-opt:_"
+      case "2.12.10" => "-opt:_"
     }}).value,	
 //
     libraryDependencies +=
@@ -140,7 +140,7 @@ lazy val root = (project in file(".")).
       "org.scala-lang.modules" % "scala-xml_2.11" % "1.0.5",
 //
     resolvers += "uuverifiers" at "http://logicrunch.research.it.uu.se/maven/",
-//    libraryDependencies += "uuverifiers" %% "princess" % "2019-11-20"
-    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
+    libraryDependencies += "uuverifiers" %% "princess" % "2020-05-01"
+//    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
 )
 //

regression-tests/horn-abstract/Answers

@@ -50,7 +50,7 @@ palindrome.nts.smt2
 sat
 (define-fun main_q0 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (and (= F C) (= E B)) (= D A)))
 (define-fun main_q1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= E F) (>= F 0)))
-(define-fun main_q2 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= F 0) (and (and (and (or (or (not (= F E)) (= D 1)) (<= E (- 1))) (or (or (>= F E) (>= (- (+ E (* (- 2) D)) F) (- 3))) (<= F (- 1)))) (or (or (>= F E) (<= F (- 1))) (>= D 1))) (or (>= E F) (<= F (- 1))))))
+(define-fun main_q2 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= F 0) (and (and (or (or (>= (- F E) 1) (>= (- (+ E (* (- 2) D)) F) (- 3))) (<= F (- 1))) (or (or (>= (- F E) 1) (<= F (- 1))) (>= D 1))) (or (>= E F) (<= F (- 1))))))
 (define-fun main_qf () Bool true)
 (define-fun palindrome_q0 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (and (and (= E A) (= F B)) (= G C)) (and (>= B 0) (>= C 0))))
 (define-fun palindrome_q1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (>= (- B C) 1) (>= C 0))))

regression-tests/horn-hcc/Answers

@@ -155,20 +155,20 @@ UNSAFE
 
 ---------------------------------------
 Init:
- Proc1(0, 0)  Proc1(0, 2)  Proc1(0, 1) 
+ Proc1(0, 2)  Proc1(0, 0)  Proc1(0, 1) 
 ---------------------------------------
       |      
       |      
       V      
- Proc2(0, 0) 
+ Proc2(2, 2) 
 ---------------------------------------
                    |      
                    |      
                    V      
-              Proc2(2, 2) 
+              Proc2(0, 0) 
 ---------------------------------------
 Final:
- Proc2(2, 0)  Proc2(2, 2)  Proc1(2, 1) 
+ Proc2(0, 2)  Proc2(0, 0)  Proc1(0, 1) 
 ---------------------------------------
 
 test-para2.hcc

regression-tests/horn-prolog/Answers

@@ -50,7 +50,7 @@ palindrome.nts.horn
 SOLVABLE
 main_q0(A,B,C,D,E,F) :- (((F = C), (E = B)), (D = A)).
 main_q1(A,B,C,D,E,F) :- ((E >= F), (F >= 0)).
-main_q2(A,B,C,D,E,F) :- ((F >= 0), (((((\+((F = E)); (D = 1)); (E =< -1)), (((F >= E); (((E + (-2 * D)) - F) >= -3)); (F =< -1))), (((F >= E); (F =< -1)); (D >= 1))), ((E >= F); (F =< -1)))).
+main_q2(A,B,C,D,E,F) :- ((F >= 0), ((((((F - E) >= 1); (((E + (-2 * D)) - F) >= -3)); (F =< -1)), ((((F - E) >= 1); (F =< -1)); (D >= 1))), ((E >= F); (F =< -1)))).
 main_qf :- true.
 palindrome_q0(A,B,C,D,E,F,G,H) :- (((((E = A), (F = B)), (G = C)), (H = D)), ((B >= 0), (C >= 0))).
 palindrome_q1(A,B,C,D,E,F,G,H) :- (((((H = D), (G = C)), (F = B)), (E = A)), (((B - C) >= 1), (C >= 0))).

regression-tests/horn-smt-lib/Answers

@@ -25,7 +25,7 @@ palindrome.nts.smt2
 sat
 (define-fun main_q0 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (and (= F C) (= E B)) (= D A)))
 (define-fun main_q1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= E F) (>= F 0)))
-(define-fun main_q2 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= F 0) (and (and (and (or (or (not (= F E)) (= D 1)) (<= E (- 1))) (or (or (>= F E) (>= (- (+ E (* (- 2) D)) F) (- 3))) (<= F (- 1)))) (or (or (>= F E) (<= F (- 1))) (>= D 1))) (or (>= E F) (<= F (- 1))))))
+(define-fun main_q2 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int)) Bool (and (>= F 0) (and (and (or (or (>= (- F E) 1) (>= (- (+ E (* (- 2) D)) F) (- 3))) (<= F (- 1))) (or (or (>= (- F E) 1) (<= F (- 1))) (>= D 1))) (or (>= E F) (<= F (- 1))))))
 (define-fun main_qf () Bool true)
 (define-fun palindrome_q0 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (and (and (= E A) (= F B)) (= G C)) (and (>= B 0) (>= C 0))))
 (define-fun palindrome_q1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int)) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (>= (- B C) 1) (>= C 0))))

src/lazabs/Main.scala

@@ -268,7 +268,7 @@ object Main {
 
 
   val greeting =
-    "Eldarica v2.0.2.\n(C) Copyright 2012-2020 Hossein Hojjat and Philipp Ruemmer"
+    "Eldarica v2.0.3.\n(C) Copyright 2012-2020 Hossein Hojjat and Philipp Ruemmer"
 
   def doMain(args: Array[String],
              stoppingCond : => Boolean) : Unit = try {