From a51f4e6cba57b6711e36ef482f4e320c9cf0542f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 18 Nov 2015 15:46:24 -0600 Subject: Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). --- Test/optimization/Optimization2.bpl.expect | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 Test/optimization/Optimization2.bpl.expect (limited to 'Test/optimization/Optimization2.bpl.expect') diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect new file mode 100644 index 00000000..cab2fd3d --- /dev/null +++ b/Test/optimization/Optimization2.bpl.expect @@ -0,0 +1,3 @@ +Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +2 type checking errors detected in Optimization2.bpl -- cgit v1.2.3