version number

uuverifiers · Feb 26, 2019 · 748a2f0 · 748a2f0
1 parent 229b00a
commit 748a2f0
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 11 deletions.
diff --git a/build.sbt b/build.sbt
@@ -2,9 +2,9 @@
 lazy val commonSettings = Seq(
     name := "Eldarica",
     organization := "uuverifiers",
-    version := "2.0-alpha1",
-    scalaVersion := "2.11.8",
-    crossScalaVersions := Seq("2.11.8", "2.12.6"),
+    version := "2.0",
+    scalaVersion := "2.11.12",
+    crossScalaVersions := Seq("2.11.12", "2.12.8"),
     publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) )
 )
 
@@ -121,8 +121,8 @@ lazy val root = (project in file(".")).
       List("-feature",
            "-language:implicitConversions,postfixOps,reflectiveCalls"),
     scalacOptions += (scalaVersion map { sv => sv match {
-      case "2.11.8" => "-optimise"
-      case "2.12.6" => "-opt:_"
+      case "2.11.12" => "-optimise"
+      case "2.12.8" => "-opt:_"
     }}).value,	
 //
     libraryDependencies +=
@@ -138,7 +138,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" % "2018-12-06"
-    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
+    libraryDependencies += "uuverifiers" %% "princess" % "2019-02-26"
+//    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
 )
 //
diff --git a/regression-tests/horn-abstract/Answers b/regression-tests/horn-abstract/Answers
@@ -196,7 +196,7 @@ sat
 (define-fun main_q2 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (and (and (and (and (>= (+ (* (- 3) F) (+ E (* (- 4) D))) (- 4294967306)) (>= (- (+ E (* (- 2) D)) F) (- 3))) (>= E F)) (<= F 2147483647)) (<= E 2147483647)))
 (define-fun main_qf () Bool true)
 (define-fun palindrome_q0 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (= E A) (or (and (and (= B F) (= C G)) (and (<= F 2147483647) (>= F G))) (and (and (= B F) (= C G)) (and (and (<= F 2147483646) (>= (- F G) (- 1))) (>= G 1))))))
-(define-fun palindrome_q1 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (and (>= (- B C) 1) (<= C 2147483647)) (<= B 2147483647))))
+(define-fun palindrome_q1 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (>= (- B C) 1) (<= B 2147483647))))
 (define-fun palindrome_q2 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (= E A) (and (and (>= (+ B (+ (* (- 3) C) (* (- 4) H))) (- 4294967302)) (>= (+ B (- (* (- 2) H) C)) (- 1))) (<= C 2147483647))))
 (define-fun palindrome_q3 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32)) (G (_ BitVec 32)) (H (_ BitVec 32))) Bool (and (and (and (= G C) (= F B)) (= E A)) (and (and (>= (- B C) (- 1)) (<= C 2147483647)) (>= C B))))
 (define-fun palindrome_q4 ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)) (E (_ BitVec 32)) (F (_ BitVec 32))) Bool (and (and (>= (+ (* (- 3) B) (+ C (* (- 4) D))) (- 4294967306)) (>= (- (+ C (* (- 2) D)) B) (- 3))) (<= B 2147483647)))

diff --git a/src/lazabs/Main.scala b/src/lazabs/Main.scala
@@ -251,7 +251,7 @@ object Main {
 
 
   val greeting =
-    "Eldarica v2.0-alpha, 2019-X.\n(C) Copyright 2012-2019 Hossein Hojjat and Philipp Ruemmer"
+    "Eldarica v2.0.\n(C) Copyright 2012-2019 Hossein Hojjat and Philipp Ruemmer"
 
   def doMain(args: Array[String],
              stoppingCond : => Boolean) : Unit = try {

diff --git a/src/lazabs/horn/parser/HornLexer.jflex b/src/lazabs/horn/parser/HornLexer.jflex
@@ -110,4 +110,4 @@ ArmcComment     = "%" {InputCharacter}* {LineTerminator}
 }
 
 
-. | \n          { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
+[^] | \n          { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
diff --git a/src/lazabs/parser/Lexer.jflex b/src/lazabs/parser/Lexer.jflex
@@ -152,4 +152,4 @@ EndOfLineComment     = "//" {InputCharacter}* {LineTerminator}
 }
 
 
-. | \n          { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
+[^] | \n          { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
Original file line number	Diff line number	Diff line change
Expand Up		@@ -110,4 +110,4 @@ ArmcComment = "%" {InputCharacter}* {LineTerminator}
		}


		. \| \n { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
		[^] \| \n { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
Original file line number	Diff line number	Diff line change
Expand Up		@@ -152,4 +152,4 @@ EndOfLineComment = "//" {InputCharacter}* {LineTerminator}
		}


		. \| \n { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }
		[^] \| \n { System.err.println("Illegal character '" + yytext() + "'" + " Scala Lexial Analyzer in " + yyline + " " + yycolumn); }