From 29959bec6e023f64cad0a5d43b18052f08ac94c5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 4 Jun 2019 14:48:21 -0700 Subject: Add check that result matches benchmark status (#3028) This commit adds a check to make sure that the result of a `(check-sat)` call matches the expected result set via `(set-info :status ...)`. In doing so, it also fixes an issue where CVC4 would crash if asked for the unsat core after setting the status to `unsat` but before calling `(check-sat)` (see regression for concrete example). This happened because CVC4 was storing the expected result and the computed result both in the same variable (the expected result wasn't really being used though). This commit keeps track of the expected result and the computed result in separate variables to fix that issue. --- test/regress/regress0/sets/mar2014/sharing-preregister.smt2 | 1 - 1 file changed, 1 deletion(-) (limited to 'test/regress/regress0/sets') diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 index d851ca35e..e3e88c65f 100644 --- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -1,6 +1,5 @@ ; EXPECT: unsat (set-logic QF_UFLIAFS) -(set-info :status sat) (declare-fun a () Int) (declare-fun b () Int) (declare-fun x () (Set Int)) -- cgit v1.2.3