summaryrefslogtreecommitdiff
path: root/test/regress/regress0/use_approx/bug812_approx.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/use_approx/bug812_approx.smt2')
-rw-r--r--test/regress/regress0/use_approx/bug812_approx.smt23
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/use_approx/bug812_approx.smt2 b/test/regress/regress0/use_approx/bug812_approx.smt2
index 4b5af6710..45908e3dd 100644
--- a/test/regress/regress0/use_approx/bug812_approx.smt2
+++ b/test/regress/regress0/use_approx/bug812_approx.smt2
@@ -1,11 +1,10 @@
; REQUIRES: glpk
; COMMAND-LINE: --use-approx
-; EXPECT: unknown
(set-logic UFNIA)
(set-info :source "Reduced from regression 'bug812.smt2' using ddSMT to exercise GLPK")
(set-info :smt-lib-version 2.6)
(set-info :category "crafted")
-(set-info :status unknown)
+(set-info :status unsat)
(declare-fun s (Int Int) Int)
(declare-fun P (Int Int Int) Int)
(declare-fun p (Int) Int)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback