From 16d5522e16a0ee01da7af388bd20a063785b6aa1 Mon Sep 17 00:00:00 2001 From: liuchangliu Date: Sun, 12 Jul 2020 18:03:10 -0400 Subject: [PATCH] fix #113. The ReachabilityResult needs to return an array of reachable sets instead of one set in the form of AbstractPolytope. --- src/satisfiability/bab.jl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/satisfiability/bab.jl b/src/satisfiability/bab.jl index a07fa9d9..e47459ae 100644 --- a/src/satisfiability/bab.jl +++ b/src/satisfiability/bab.jl @@ -39,13 +39,14 @@ function solve(solver::BaB, problem::Problem) return interpret_result(reach, bound, problem.output, x_l, x_u) end +# This function is used by BaB and Sherlock function interpret_result(reach, bound, output, x_l, x_u) if high(reach) < high(output) && low(reach) > low(output) return ReachabilityResult(:holds, [reach]) end high(bound) > high(output) && return CounterExampleResult(:violated, x_u) low(bound) < low(output) && return CounterExampleResult(:violated, x_l) - return ReachabilityResult(:unknown, reach) + return ReachabilityResult(:unknown, [reach]) end function output_bound(solver::BaB, problem::Problem, type::Symbol)