From 1229469155cbe910ca56e546f0ae31a6792a9e4d Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 30 Dec 2024 10:16:46 -0800 Subject: [PATCH] update golds --- SBVTestSuite/GoldFiles/allSat8.gold | 2 -- SBVTestSuite/GoldFiles/nested1.gold | 3 --- SBVTestSuite/GoldFiles/nested2.gold | 3 --- SBVTestSuite/GoldFiles/nested3.gold | 3 --- SBVTestSuite/GoldFiles/nested4.gold | 3 --- SBVTestSuite/GoldFiles/noOpt1.gold | 3 --- SBVTestSuite/GoldFiles/noOpt2.gold | 3 --- 7 files changed, 20 deletions(-) diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold index a42103f1..d71c83f6 100644 --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -59,5 +59,3 @@ EXCEPTION CAUGHT: *** *** NB. If this is a use case you'd like SBV to support, please get in touch! -CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1647:57 in sbv-11.0.5-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold index 8c873d31..d3cc36c8 100644 --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -9,6 +9,3 @@ Data.SBV: Mismatched contexts detected. *** while another one is in execution, or use results from one such call in another. *** Please avoid such nested calls, all interactions should be from the same context. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1928:48 in sbv-11.0.5-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold index 8c873d31..d3cc36c8 100644 --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -9,6 +9,3 @@ Data.SBV: Mismatched contexts detected. *** while another one is in execution, or use results from one such call in another. *** Please avoid such nested calls, all interactions should be from the same context. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1928:48 in sbv-11.0.5-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold index bd0714d1..bbcf540a 100644 --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -32,6 +32,3 @@ Data.SBV: Mismatched contexts detected. *** while another one is in execution, or use results from one such call in another. *** Please avoid such nested calls, all interactions should be from the same context. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1928:48 in sbv-11.0.5-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold index 8c873d31..d3cc36c8 100644 --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -9,6 +9,3 @@ Data.SBV: Mismatched contexts detected. *** while another one is in execution, or use results from one such call in another. *** Please avoid such nested calls, all interactions should be from the same context. *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1928:48 in sbv-11.0.5-inplace:Data.SBV.Core.Symbolic \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/noOpt1.gold b/SBVTestSuite/GoldFiles/noOpt1.gold index 65f121b4..7ac2eb7e 100644 --- a/SBVTestSuite/GoldFiles/noOpt1.gold +++ b/SBVTestSuite/GoldFiles/noOpt1.gold @@ -26,6 +26,3 @@ *** Data.SBV: Unsupported call to optimize when no objectives are present. *** Use "sat" for plain satisfaction - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Provers/Prover.hs:265:27 in sbv-11.0.5-inplace:Data.SBV.Provers.Prover \ No newline at end of file diff --git a/SBVTestSuite/GoldFiles/noOpt2.gold b/SBVTestSuite/GoldFiles/noOpt2.gold index 74a653c5..b11a9961 100644 --- a/SBVTestSuite/GoldFiles/noOpt2.gold +++ b/SBVTestSuite/GoldFiles/noOpt2.gold @@ -28,6 +28,3 @@ *** Data.SBV: Unsupported call sat/prove when optimization objectives are present. *** Use "optimize"/"optimizeWith" to calculate optimal satisfaction! - -CallStack (from HasCallStack): - error, called at ./Data/SBV/Provers/Prover.hs:612:33 in sbv-11.0.5-inplace:Data.SBV.Provers.Prover \ No newline at end of file