From 2cddab3e5f1d5b0ee2017f67b30fbcd0b2271f7d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 27 Jan 2025 14:11:22 +0100 Subject: [PATCH] test: Make sure qfbv-timeout actually times out --- tests/bitv/testfile-qfbv-timeout.unix.smt2 | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/bitv/testfile-qfbv-timeout.unix.smt2 b/tests/bitv/testfile-qfbv-timeout.unix.smt2 index 27fcf0299..7dce2d46d 100644 --- a/tests/bitv/testfile-qfbv-timeout.unix.smt2 +++ b/tests/bitv/testfile-qfbv-timeout.unix.smt2 @@ -1,5 +1,10 @@ (set-info :smt-lib-version 2.6) (set-option :reproducible-resource-limit 1) +; We want this test to loop during assertions, which it only does +; if we are trying to generate a model. +; This is somewhat brittle though and we should probably switch to a better +; behaving looping problem. +(set-option :produce-models true) (set-logic QF_BV) (set-info :source | Patrice Godefroid, SAGE (systematic dynamic test generation)