Skip to content

Commit

Permalink
update golds
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Dec 30, 2024
1 parent 43cf5d3 commit 1229469
Show file tree
Hide file tree
Showing 7 changed files with 0 additions and 20 deletions.
2 changes: 0 additions & 2 deletions SBVTestSuite/GoldFiles/allSat8.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/nested1.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/nested2.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/nested3.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/nested4.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/noOpt1.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions SBVTestSuite/GoldFiles/noOpt2.gold
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 1229469

Please sign in to comment.