Skip to content

Commit

Permalink
test: Make sure qfbv-timeout actually times out
Browse files Browse the repository at this point in the history
  • Loading branch information
bclement-ocp committed Jan 27, 2025
1 parent bc072d2 commit 2cddab3
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions tests/bitv/testfile-qfbv-timeout.unix.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down

0 comments on commit 2cddab3

Please sign in to comment.