Merge branch 'master' into external-predicate-gen

uuverifiers · Feb 28, 2024 · a3f44fd · a3f44fd
2 parents 3528dea + ca5237d
commit a3f44fd
Show file tree

Hide file tree

Showing 12 changed files with 399 additions and 186 deletions.
diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
@@ -23,5 +23,5 @@ jobs:
     - name: UnitTests
       run: sbt test
     - name: Test
-      run: cd regression-tests; export TERM=xterm; wget http://logicrunch.it.uu.se:4096/~philipp/yices; chmod +x yices; export PATH=`pwd`:$PATH; ./runalldirs
+      run: cd regression-tests; export TERM=xterm; wget https://eldarica.org/yices; chmod +x yices; export PATH=`pwd`:$PATH; ./runalldirs
 
diff --git a/AUTHORS b/AUTHORS
@@ -7,4 +7,5 @@ Further contributors:
 
 Zafer Esen <[email protected]>
 Filip Konecny <[email protected]>
-Pavle Subotic <[email protected]>
+Pavle Subotic <[email protected]>
+Gambhir Sankalp <[email protected]>
diff --git a/README.md b/README.md
@@ -22,9 +22,7 @@ with further contributions by Zafer Esen, Filip Konecny, and Pavle Subotic.
 
 There is a simple **web interface** to experiment with the C interface
 of Eldarica:
-http://logicrunch.it.uu.se:4096/~wv/eldarica
-
-The latest **nightly build** is available from: http://logicrunch.it.uu.se:4096/~wv/eldarica/eldarica-bin-nightly.zip
+https://eldarica.org/eldarica
 
 Documentation
 -------------
@@ -44,7 +42,7 @@ When using a binary release, one can instead also call
 
   <code>java -jar target/scala-2.\*/Eldarica-assembly\*.jar regression-tests/horn-smt-lib/rate_limiter.c.nts.smt2</code>
 
-A set of examples is provided on http://logicrunch.it.uu.se:4096/~wv/eldarica, and included
+A set of examples is provided on https://eldarica.org/eldarica, and included
 in the distributions directory <code>regression-tests</code>.
 
 You can use the script <code>eld-client</code> instead of

diff --git a/build.sbt b/build.sbt
@@ -6,7 +6,7 @@ lazy val commonSettings = Seq(
     homepage := Some(url("https://github.com/uuverifiers/eldarica")),
     licenses := Seq("BSD License 2.0" -> url("https://github.com/uuverifiers/eldarica/blob/master/LICENSE")),
     scalaVersion := "2.11.12",
-    crossScalaVersions := Seq("2.11.12", "2.12.17"),
+    crossScalaVersions := Seq("2.11.12", "2.12.18"),
     run / fork := true,
     cancelable in Global := true,
     publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) )
@@ -125,7 +125,7 @@ lazy val root = (project in file(".")).
            "-encoding", "UTF-8"),
     scalacOptions += (scalaVersion map { sv => sv match {
       case "2.11.12" => "-optimise"
-      case "2.12.17" => "-opt:_"
+      case "2.12.18" => "-opt:_"
     }}).value,
 //
     assembly / test := None,
@@ -150,7 +150,7 @@ lazy val root = (project in file(".")).
 //
 //    libraryDependencies += "io.github.uuverifiers" %% "princess" % "2023-04-07"
 //
-    resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/").withAllowInsecureProtocol(true),
+    resolvers += "uuverifiers" at "https://eldarica.org/maven/",
     libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
 
 )

diff --git a/regression-tests/special/Answers b/regression-tests/special/Answers
@@ -38,3 +38,6 @@ sat
 (define-fun inv_main7 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D) (= (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) A)) (= (newAddr (alloc emptyHeap (O_node var1))) B)))) (= B C)))
 (define-fun inv_main8 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (= (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D (O_node (node B (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D)))))) A) (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) B (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) B)))))) B))) 0))) (O_node var0))) D) (= (newAddr (alloc emptyHeap (O_node var1))) B))))) (= B C)))
 (define-fun inv_main9 ((A Heap) (B Addr) (C Addr) (D Addr)) Bool (and (exists ((var0 node)) (exists ((var1 node)) (and (= (write (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D (O_node (node C (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D)))))) D (O_node (node (L (getnode (read (write (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D (O_node (node C (R (getnode (read (newHeap (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D)))))) D))) 0))) A) (and (= (newAddr (alloc (write (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C (O_node (node (L (getnode (read (write (newHeap (alloc emptyHeap (O_node var1))) C (O_node (node 0 (R (getnode (read (newHeap (alloc emptyHeap (O_node var1))) C)))))) C))) 0))) (O_node var0))) D) (= (newAddr (alloc emptyHeap (O_node var1))) C))))) (= C B)))
+
+amotsa.smt2
+sat