Disallow separation logic in incremental mode (#7888)

Fixes #5541. Fixes #5607.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 9f4e054093e85550c8d5365843a5ee634abc5450..4bb3bfabf8cb3bb3f5561cffd1a787be11bf562a 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1219,6 +1219,13 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
   }
   SolverEngineScope smts(this);
   finishInit();
+  // check whether incremental is enabled, where separation logic is not
+  // supported.
+  if (d_env->getOptions().base.incrementalSolving)
+  {
+    throw RecoverableModalException(
+        "Separation logic not supported in incremental mode");
+  }
   TheoryEngine* te = getTheoryEngine();
   te->declareSepHeap(locT, dataT);
 }

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index bdd8201bc504b2e6e3a6841f2737204a28a9d3ea..7a04566ddd04120dcfc9d9a22f8b1587fbb9f364 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1902,6 +1902,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
 TEST_F(TestApiBlackSolver, declareSepHeap)
 {
   d_solver.setLogic("ALL");
+  d_solver.setOption("incremental", "false");
   Sort integer = d_solver.getIntegerSort();
   ASSERT_NO_THROW(d_solver.declareSepHeap(integer, integer));
   // cannot declare separation logic heap more than once

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 7313405be2dfb61d90e8d6b467b87505dcb1ccf9..2de49dfb47911d0d7a54886250a9be3f491a49f7 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1879,6 +1879,7 @@ class SolverTest
   @Test void declareSepHeap() throws CVC5ApiException
   {
     d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
     Sort integer = d_solver.getIntegerSort();
     assertDoesNotThrow(() -> d_solver.declareSepHeap(integer, integer));
     // cannot declare separation logic heap more than once

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 90e6610d85daa1b373ab784e530f348c00a2cf82..b73b691c4208b9e3e07e2723e81ce63003a3790d 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1338,6 +1338,7 @@ def test_get_value3(solver):
 
 def test_declare_sep_heap(solver):
     solver.setLogic("ALL")
+    solver.setOption("incremental", "false")
     integer = solver.getIntegerSort()
     solver.declareSepHeap(integer, integer)
     # cannot declare separation logic heap more than once
@@ -2100,16 +2101,6 @@ def test_declare_pool(solver):
     with pytest.raises(RuntimeError):
         solver.declarePool("i", nullSort, [])
 
-
-def test_declare_sep_heap(solver):
-    solver.setLogic("ALL")
-    integer = solver.getIntegerSort()
-    solver.declareSepHeap(integer, integer)
-    # cannot declare separation logic heap more than once
-    with pytest.raises(RuntimeError):
-        solver.declareSepHeap(integer, integer)
-
-
 def test_define_fun_global(solver):
     bSort = solver.getBooleanSort()