From cafdeec088c5c336d36d6cf3a1ce23824d7c37d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 16 Apr 2024 15:57:28 -0400 Subject: [PATCH] test: c1 works with bitwuzla, not with yices (because returned witnesses are not deterministic accross solvers) --- test.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/test.py b/test.py index fa30707..f2f752e 100755 --- a/test.py +++ b/test.py @@ -209,10 +209,11 @@ def test_s2(self): def test_c1(self): """ SD-SPI driver from ZipCPU. Missing condition in `if`. Fails after 101 cycles. """ - # TODO: why does this fail now? + # fails with yices self.synth_cannot_repair(zip_cpu_sdspi_dir, "c1", solver="yices2", init="zero", incremental=True, timeout=120) - #changes = self.synth_success(zip_cpu_sdspi_dir, "c1", solver="yices2", init="zero", incremental=True, timeout=120) - #self.assertEqual(changes, 1) + # succeeds with bitwuzla + changes = self.synth_success(zip_cpu_sdspi_dir, "c1", solver="bitwuzla", init="zero", incremental=True, timeout=120) + self.assertEqual(changes, 1) def test_c3(self): """ SD-SPI driver from ZipCPU. Missing delay register. Fails after 6 cycles. """