diff options
Diffstat (limited to 'test/regress/regress0/bug322.cvc.smt2')
| -rw-r--r-- | test/regress/regress0/bug322.cvc.smt2 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/bug322.cvc.smt2 b/test/regress/regress0/bug322.cvc.smt2 new file mode 100644 index 000000000..62c04579c --- /dev/null +++ b/test/regress/regress0/bug322.cvc.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-datatypes ((UNIT 0)) (((Unit)))) +(declare-datatypes ((BOOL 0)) (((Truth) (Falsity)))) +(declare-sort node$type 0) +(declare-sort value$type 0) + +(declare-sort Nodes$t$type 0) + + +(define-fun is_faulty ((p node$type) (deliver (Array node$type (Array node$type BOOL)))) BOOL (ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) Truth Falsity)) +(check-sat) |