From 9f567a62151e0dac1b4c19410a4b0593623b1cfc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Nov 2017 19:38:47 -0800
Subject: [PATCH] fix example file to be smt2 format
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
examples/maxsat/ex.smt | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/examples/maxsat/ex.smt b/examples/maxsat/ex.smt
index 14ac0db89..d28b27c80 100644
--- a/examples/maxsat/ex.smt
+++ b/examples/maxsat/ex.smt
@@ -1,11 +1,11 @@
-(benchmark ex
- :logic AUFLIA
- :extrafuns ((x Int) (y Int) (z Int))
- :assumption (> x 0)
- :assumption (<= x -1)
- :assumption (or (> x 0) (< y 1))
- :assumption (> y 2)
- :assumption (> y 3)
- :assumption (<= y -1)
- :formula (= z (+ x y)))
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert-soft (> x 0))
+(assert-soft (<= x -1))
+(assert-soft (or (> x 0) (< y 1)))
+(assert-soft (> y 2))
+(assert-soft (> y 3))
+(assert-soft (<= y -1))
+(assert (= z (+ x y)))
\ No newline at end of file