aboutsummaryrefslogtreecommitdiff
path: root/test.smt2
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--test.smt27
1 files changed, 7 insertions, 0 deletions
diff --git a/test.smt2 b/test.smt2
new file mode 100644
index 0000000..79d05c6
--- /dev/null
+++ b/test.smt2
@@ -0,0 +1,7 @@
+(declare-const x_0 Real)
+(declare-const x_1 Real)
+(define-fun net_a () Real (+ (* x_0 2) 3))
+(define-fun net_b () Real (+ 3 (* 2 x_0)))
+(assert (> (abs (- net_a net_b)) 0.0000100000))
+(check-sat)
+(get-model)