From c82167350a4752c4282b18a1cdbac1312c154e7b Mon Sep 17 00:00:00 2001 From: Oliver Westphal Date: Thu, 20 Jul 2023 13:52:59 +0200 Subject: [PATCH] fix unfolding one to many times --- src/Test/IOTasks/Z3.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Test/IOTasks/Z3.hs b/src/Test/IOTasks/Z3.hs index c824adc..be2d278 100644 --- a/src/Test/IOTasks/Z3.hs +++ b/src/Test/IOTasks/Z3.hs @@ -123,7 +123,7 @@ satPathsQ nVar to t maxUnfolds maxSeqLength checkOverflows q = do _ -> satPaths' nUnfolds (nInputs+1) to t (SomeConstraint c:s,d+1) q -- stores constraints in reversed order satPaths' nUnfolds nInputs to (Assert c t) (s,d) q = satPaths' nUnfolds nInputs to t (SomeConstraint c:s,d+1) q -- stores constraints in reversed order satPaths' nUnfolds nInputs to (Unfold t) (s,d) q - | nUnfolds <= maxUnfolds = satPaths' (nUnfolds+1) nInputs to t (s,d) q + | nUnfolds < maxUnfolds = satPaths' (nUnfolds+1) nInputs to t (s,d) q | otherwise = pure () data ValueGenerator where