diff options
Diffstat (limited to 'test/regress/regress1/sygus/simple-rewrite-in-db.sy')
| -rw-r--r-- | test/regress/regress1/sygus/simple-rewrite-in-db.sy | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/simple-rewrite-in-db.sy b/test/regress/regress1/sygus/simple-rewrite-in-db.sy new file mode 100644 index 000000000..46d3b59b0 --- /dev/null +++ b/test/regress/regress1/sygus/simple-rewrite-in-db.sy @@ -0,0 +1,15 @@ +; COMMAND-LINE: --sygus-si=all --sygus-out=status +; EXPECT: unsat + +(set-logic UF) + +(synth-fun f ((x Bool) (y Bool)) Bool + ((Start Bool)) + ((Start Bool (true false x y (not Start) (= Start Start))))) + +(declare-var x Bool) +(declare-var y Bool) + +(constraint (= (f x y) (xor x y))) + +(check-synth) |