diff options
Diffstat (limited to 'test/regress/regress0/sygus/ccp16.lus.sy')
-rw-r--r-- | test/regress/regress0/sygus/ccp16.lus.sy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy new file mode 100644 index 000000000..662069105 --- /dev/null +++ b/test/regress/regress0/sygus/ccp16.lus.sy @@ -0,0 +1,72 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SAT) + +(define-fun + __node_init_top_0 ( + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + ) Bool + + (and (= top.usr.OK_a_0 true) top.res.init_flag_a_0) +) + +(define-fun + __node_trans_top_0 ( + (top.usr.OK_a_1 Bool) + (top.res.init_flag_a_1 Bool) + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + ) Bool + + (and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1)) +) + + + +(synth-inv str_invariant( + (top.usr.OK Bool) + (top.res.init_flag Bool) +)) + + +(declare-primed-var top.usr.OK Bool) +(declare-primed-var top.res.init_flag Bool) + +(define-fun + init ( + (top.usr.OK Bool) + (top.res.init_flag Bool) + ) Bool + + (and (= top.usr.OK true) top.res.init_flag) +) + +(define-fun + trans ( + + ;; Current state. + (top.usr.OK Bool) + (top.res.init_flag Bool) + + ;; Next state. + (top.usr.OK! Bool) + (top.res.init_flag! Bool) + + ) Bool + + (and (= top.usr.OK! true) (not top.res.init_flag!)) +) + +(define-fun + prop ( + (top.usr.OK Bool) + (top.res.init_flag Bool) + ) Bool + + top.usr.OK +) + +(inv-constraint str_invariant init trans prop) + +(check-synth) |