1.13.9: Fix of embarrassing unsoundness (see CHANGELOG)

rindPHI · Apr 27, 2023 · 83f1d04 · 83f1d04
1 parent 4a9cb0e
commit 83f1d04
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 3 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,6 +5,12 @@ This file contains the notable changes in the ISLa project since version 0.2a1
 
 ## [unreleased]
 
+## [1.13.9] - 2023-04-27
+
+### Changed
+
+- Bug fix to HUGE unsoundness: Solver returned a solution for "false" constraint.
+
 ## [1.13.8] - 2023-04-27
 
 ### Changed

diff --git a/pyproject.toml b/pyproject.toml
@@ -8,7 +8,7 @@ build-backend = "setuptools.build_meta"
 
 [project]
 name = "isla-solver"
-version = "1.13.8"
+version = "1.13.9"
 authors = [
     { name = "Dominic Steinhoefel", email = "[email protected]" },
 ]

diff --git a/src/isla/__init__.py b/src/isla/__init__.py
@@ -16,4 +16,4 @@
 # You should have received a copy of the GNU General Public License
 # along with ISLa.  If not, see <http://www.gnu.org/licenses/>.
 
-__version__ = "1.13.8"
+__version__ = "1.13.9"
diff --git a/src/isla/solver.py b/src/isla/solver.py
@@ -574,7 +574,7 @@ def __init__(
             self.top_constant.map(
                 lambda c: self.formula.substitute_expressions({c: self.initial_tree})
             )
-            .orelse(lambda: true())
+            .orelse(lambda: self.formula)
             .get()
         )
         initial_state = SolutionState(initial_formula, self.initial_tree)

diff --git a/tests/test_solver.py b/tests/test_solver.py
@@ -102,6 +102,16 @@
 
 
 class TestSolver(unittest.TestCase):
+    def test_no_solution_for_literal_false_constraint(self):
+        # Yes, this happened
+        solver = ISLaSolver(LANG_GRAMMAR, "false")
+
+        try:
+            solver.solve()
+            self.fail("There should be no solution here")
+        except StopIteration:
+            pass
+
     def test_atomic_smt_formula(self):
         assgn = language.Constant("$assgn", "<assgn>")
         formula = language.SMTFormula(