summaryrefslogtreecommitdiff
path: root/examples/nra-translate/nra-translate-example-input.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'examples/nra-translate/nra-translate-example-input.smt2')
-rw-r--r--examples/nra-translate/nra-translate-example-input.smt211
1 files changed, 11 insertions, 0 deletions
diff --git a/examples/nra-translate/nra-translate-example-input.smt2 b/examples/nra-translate/nra-translate-example-input.smt2
new file mode 100644
index 000000000..229c46d4a
--- /dev/null
+++ b/examples/nra-translate/nra-translate-example-input.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status sat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (+ x n) 0))
+(assert (= (+ y n) 1))
+
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback