aboutsummaryrefslogtreecommitdiff
path: root/test.smt2
diff options
context:
space:
mode:
authorericmarin <maarin.eric@gmail.com>2026-03-10 11:05:26 +0100
committerericmarin <maarin.eric@gmail.com>2026-03-10 12:05:35 +0100
commit7933d744e06337f1d69b7da83f2cee1611556097 (patch)
tree2a1594ab6f8d2cfeb784dee80e2d830d9999e4a5 /test.smt2
parent51cd389b4e322313671dd0e53513ce84b72a1652 (diff)
downloadvein-7933d744e06337f1d69b7da83f2cee1611556097.tar.gz
vein-7933d744e06337f1d69b7da83f2cee1611556097.zip
added prover script
Diffstat (limited to 'test.smt2')
-rw-r--r--test.smt27
1 files changed, 0 insertions, 7 deletions
diff --git a/test.smt2 b/test.smt2
deleted file mode 100644
index 79d05c6..0000000
--- a/test.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(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)