Skip to content

Commit

Permalink
Fix timelimit per goal (#984)
Browse files Browse the repository at this point in the history 
* Stop process decl as soon as a status is printed

* Update tests
  • Loading branch information
@Stevendeo
Stevendeo authored Nov 29, 2023
1 parent 6ef54f4 commit 2cf6df2
Show file tree
Hide file tree
Showing 4 changed files with 97 additions and 4 deletions.
13 changes: 9 additions & 4 deletions src/bin/common/solving_loop.ml
View file
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
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
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

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

0 comments on commit 2cf6df2

Please sign in to comment.