Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix timelimit per goal #984

Merged
merged 2 commits into from
Nov 29, 2023
Merged

Fix timelimit per goal #984

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
56aa85c
Stop process decl as soon as a status is printed
Stevendeo Nov 28, 2023
d258ec8
Update tests
Stevendeo Nov 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,8 @@ type solve_res =
| Unknown of model option
| Unsat

exception StopProcessDecl

let main () =
let () = Dolmen_loop.Code.init [] in

Expand All @@ -154,12 +156,15 @@ let main () =
match status with
| Timeout _ when not (Options.get_timelimit_per_goal ()) ->
exit_as_timeout ()
| _ -> ()
| _ -> raise StopProcessDecl
in
let () =
List.iter
(FE.process_decl ~hook_on_status ftdn_env)
cnf
try
List.iter
(FE.process_decl ~hook_on_status ftdn_env)
cnf
with
| StopProcessDecl -> ()
in
if Options.get_timelimit_per_goal() then
Options.Time.unset_timeout ();
Expand Down
9 changes: 9 additions & 0 deletions tests/bitv/testfile-qfbv-timeout.dolmen.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@

unknown
(:reason-unknown (:timeout :assume))

unknown
(:reason-unknown (:timeout :assume))

unknown
(:reason-unknown (:timeout :assume))
58 changes: 58 additions & 0 deletions tests/bitv/testfile-qfbv-timeout.dolmen.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
(set-info :smt-lib-version 2.6)
(set-option :reproducible-resource-limit 1)
(set-logic QF_BV)
(set-info :source |
Patrice Godefroid, SAGE (systematic dynamic test generation)
For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun T4_11167 () (_ BitVec 32))
(declare-fun T2_10410 () (_ BitVec 16))
(declare-fun T2_10408 () (_ BitVec 16))
(declare-fun T2_10475 () (_ BitVec 16))
(declare-fun T2_10473 () (_ BitVec 16))
(declare-fun T2_10532 () (_ BitVec 16))
(declare-fun T2_10530 () (_ BitVec 16))
(declare-fun T2_10606 () (_ BitVec 16))
(declare-fun T2_10604 () (_ BitVec 16))
(declare-fun T2_10669 () (_ BitVec 16))
(declare-fun T2_10667 () (_ BitVec 16))
(declare-fun T2_10734 () (_ BitVec 16))
(declare-fun T2_10736 () (_ BitVec 16))
(declare-fun T1_11167 () (_ BitVec 8))
(declare-fun T1_11168 () (_ BitVec 8))
(declare-fun T1_11169 () (_ BitVec 8))
(declare-fun T1_11170 () (_ BitVec 8))
(declare-fun T1_10736 () (_ BitVec 8))
(declare-fun T1_10737 () (_ BitVec 8))
(declare-fun T1_10734 () (_ BitVec 8))
(declare-fun T1_10735 () (_ BitVec 8))
(declare-fun T1_10669 () (_ BitVec 8))
(declare-fun T1_10670 () (_ BitVec 8))
(declare-fun T1_10667 () (_ BitVec 8))
(declare-fun T1_10668 () (_ BitVec 8))
(declare-fun T1_10606 () (_ BitVec 8))
(declare-fun T1_10607 () (_ BitVec 8))
(declare-fun T1_10604 () (_ BitVec 8))
(declare-fun T1_10605 () (_ BitVec 8))
(declare-fun T1_10532 () (_ BitVec 8))
(declare-fun T1_10533 () (_ BitVec 8))
(declare-fun T1_10530 () (_ BitVec 8))
(declare-fun T1_10531 () (_ BitVec 8))
(declare-fun T1_10475 () (_ BitVec 8))
(declare-fun T1_10476 () (_ BitVec 8))
(declare-fun T1_10473 () (_ BitVec 8))
(declare-fun T1_10474 () (_ BitVec 8))
(declare-fun T1_10410 () (_ BitVec 8))
(declare-fun T1_10411 () (_ BitVec 8))
(declare-fun T1_10408 () (_ BitVec 8))
(declare-fun T1_10409 () (_ BitVec 8))
(assert (let ((?v_0 (bvadd T4_11167 (_ bv4 32))) (?v_12 ((_ zero_extend 16) T2_10408))) (let ((?v_10 (bvadd ?v_0 (bvsub (bvadd (bvadd (bvadd ?v_0 (_ bv61 32)) ?v_12) ((_ zero_extend 16) T2_10410)) ?v_0)))) (let ((?v_1 (bvadd ?v_10 (_ bv4 32))) (?v_18 ((_ zero_extend 16) T2_10473))) (let ((?v_16 (bvadd ?v_1 (bvsub (bvadd (bvadd (bvadd ?v_1 (_ bv53 32)) ?v_18) ((_ zero_extend 16) T2_10475)) ?v_1)))) (let ((?v_2 (bvadd ?v_16 (_ bv4 32))) (?v_24 ((_ zero_extend 16) T2_10530))) (let ((?v_22 (bvadd ?v_2 (bvsub (bvadd (bvadd (bvadd ?v_2 (_ bv70 32)) ?v_24) ((_ zero_extend 16) T2_10532)) ?v_2)))) (let ((?v_3 (bvadd ?v_22 (_ bv4 32))) (?v_30 ((_ zero_extend 16) T2_10604))) (let ((?v_28 (bvadd ?v_3 (bvsub (bvadd (bvadd (bvadd ?v_3 (_ bv59 32)) ?v_30) ((_ zero_extend 16) T2_10606)) ?v_3)))) (let ((?v_4 (bvadd ?v_28 (_ bv4 32))) (?v_36 ((_ zero_extend 16) T2_10667))) (let ((?v_34 (bvadd ?v_4 (bvsub (bvadd (bvadd (bvadd ?v_4 (_ bv63 32)) ?v_36) ((_ zero_extend 16) T2_10669)) ?v_4)))) (let ((?v_5 (bvadd ?v_34 (_ bv4 32)))) (let ((?v_40 (bvadd ?v_5 (_ bv42 32))) (?v_39 ((_ zero_extend 16) T2_10734)) (?v_38 (bvadd ?v_4 (_ bv42 32))) (?v_37 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_5) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_35 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_34) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_33 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_40) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_32 (bvadd ?v_3 (_ bv42 32))) (?v_31 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_4) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_29 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_28) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_27 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_38) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_26 (bvadd ?v_2 (_ bv42 32))) (?v_25 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_3) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_23 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_22) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_21 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_32) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_20 (bvadd ?v_1 (_ bv42 32))) (?v_19 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_2) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_17 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_16) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_15 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_26) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_14 (bvadd ?v_0 (_ bv42 32))) (?v_13 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_1) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_11 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_10) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_9 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_20) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_8 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_0) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_7 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) T4_11167) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_6 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_14) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (and true (= T2_10408 (bvor (bvshl ((_ zero_extend 8) T1_10409) (_ bv8 16)) ((_ zero_extend 8) T1_10408))) (= T2_10410 (bvor (bvshl ((_ zero_extend 8) T1_10411) (_ bv8 16)) ((_ zero_extend 8) T1_10410))) (= T2_10473 (bvor (bvshl ((_ zero_extend 8) T1_10474) (_ bv8 16)) ((_ zero_extend 8) T1_10473))) (= T2_10475 (bvor (bvshl ((_ zero_extend 8) T1_10476) (_ bv8 16)) ((_ zero_extend 8) T1_10475))) (= T2_10530 (bvor (bvshl ((_ zero_extend 8) T1_10531) (_ bv8 16)) ((_ zero_extend 8) T1_10530))) (= T2_10532 (bvor (bvshl ((_ zero_extend 8) T1_10533) (_ bv8 16)) ((_ zero_extend 8) T1_10532))) (= T2_10604 (bvor (bvshl ((_ zero_extend 8) T1_10605) (_ bv8 16)) ((_ zero_extend 8) T1_10604))) (= T2_10606 (bvor (bvshl ((_ zero_extend 8) T1_10607) (_ bv8 16)) ((_ zero_extend 8) T1_10606))) (= T2_10667 (bvor (bvshl ((_ zero_extend 8) T1_10668) (_ bv8 16)) ((_ zero_extend 8) T1_10667))) (= T2_10669 (bvor (bvshl ((_ zero_extend 8) T1_10670) (_ bv8 16)) ((_ zero_extend 8) T1_10669))) (= T2_10734 (bvor (bvshl ((_ zero_extend 8) T1_10735) (_ bv8 16)) ((_ zero_extend 8) T1_10734))) (= T2_10736 (bvor (bvshl ((_ zero_extend 8) T1_10737) (_ bv8 16)) ((_ zero_extend 8) T1_10736))) (= T4_11167 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_11170) (_ bv8 32)) ((_ zero_extend 24) T1_11169)) (_ bv8 32)) ((_ zero_extend 24) T1_11168)) (_ bv8 32)) ((_ zero_extend 24) T1_11167))) (bvslt (bvadd ?v_5 (bvsub (bvadd (bvadd (bvadd ?v_5 (_ bv64 32)) ?v_39) ((_ zero_extend 16) T2_10736)) ?v_5)) (_ bv0 32)) (bvult (_ bv0 32) ?v_6) (bvule (_ bv0 32) ?v_6) (bvult (_ bv0 32) ?v_7) (bvule (_ bv0 32) ?v_7) (bvult (_ bv0 32) ?v_8) (bvule (_ bv0 32) ?v_8) (bvult (_ bv0 32) ?v_9) (bvule (_ bv0 32) ?v_9) (bvult (_ bv0 32) ?v_11) (bvule (_ bv0 32) ?v_11) (= ?v_12 (_ bv0 32)) (bvult (_ bv0 32) ?v_13) (bvule (_ bv0 32) ?v_13) (not (= ?v_14 (_ bv4294967295 32))) (bvule (_ bv0 32) T4_11167) (not (= T4_11167 (_ bv11151 32))) (bvule T4_11167 (_ bv11151 32)) (not (= T4_11167 (_ bv4294967295 32))) (bvult (_ bv0 32) ?v_15) (bvule (_ bv0 32) ?v_15) (bvult (_ bv0 32) ?v_17) (bvule (_ bv0 32) ?v_17) (= ?v_18 (_ bv0 32)) (not (= ?v_0 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_0) (bvult (_ bv0 32) ?v_19) (bvule (_ bv0 32) ?v_19) (not (= ?v_20 (_ bv4294967295 32))) (not (= ?v_10 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_10) (bvult (_ bv0 32) ?v_21) (bvule (_ bv0 32) ?v_21) (bvult (_ bv0 32) ?v_23) (bvule (_ bv0 32) ?v_23) (= ?v_24 (_ bv0 32)) (not (= ?v_1 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_1) (bvult (_ bv0 32) ?v_25) (bvule (_ bv0 32) ?v_25) (not (= ?v_26 (_ bv4294967295 32))) (not (= ?v_16 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_16) (bvult (_ bv0 32) ?v_27) (bvule (_ bv0 32) ?v_27) (bvult (_ bv0 32) ?v_29) (bvule (_ bv0 32) ?v_29) (= ?v_30 (_ bv0 32)) (not (= ?v_2 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_2) (bvult (_ bv0 32) ?v_31) (bvule (_ bv0 32) ?v_31) (not (= ?v_32 (_ bv4294967295 32))) (not (= ?v_22 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_22) (bvult (_ bv0 32) ?v_33) (bvule (_ bv0 32) ?v_33) (bvult (_ bv0 32) ?v_35) (bvule (_ bv0 32) ?v_35) (= ?v_36 (_ bv0 32)) (not (= ?v_3 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_3) (bvult (_ bv0 32) ?v_37) (bvule (_ bv0 32) ?v_37) (not (= ?v_38 (_ bv4294967295 32))) (not (= ?v_28 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_28) (= ?v_39 (_ bv0 32)) (not (= ?v_4 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_4) (not (= ?v_40 (_ bv4294967295 32))) (not (= ?v_34 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_34) (not (= ?v_5 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_5))))))))))))))))))
(check-sat)
(get-info :reason-unknown)
(check-sat)
(get-info :reason-unknown)
(check-sat)
(get-info :reason-unknown)
(exit)
21 changes: 21 additions & 0 deletions tests/dune.inc
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading