18
18
import java .util .concurrent .Future ;
19
19
import java .util .concurrent .TimeUnit ;
20
20
import org .junit .Test ;
21
- import org .sosy_lab .common .ShutdownManager ;
22
- import org .sosy_lab .common .ShutdownNotifier ;
23
- import org .sosy_lab .common .configuration .Configuration ;
24
21
import org .sosy_lab .common .configuration .InvalidConfigurationException ;
25
- import org .sosy_lab .common .log .LogManager ;
26
- import org .sosy_lab .java_smt .SolverContextFactory ;
27
22
import org .sosy_lab .java_smt .SolverContextFactory .Solvers ;
28
23
import org .sosy_lab .java_smt .api .BasicProverEnvironment ;
29
24
import org .sosy_lab .java_smt .api .BooleanFormula ;
@@ -53,7 +48,8 @@ public void allLocalTest() throws InterruptedException, SolverException {
53
48
54
49
@ SuppressWarnings ("resource" )
55
50
@ Test
56
- public void nonlocalContext () throws ExecutionException , InterruptedException , SolverException {
51
+ public void nonlocalContextTest ()
52
+ throws ExecutionException , InterruptedException , SolverException {
57
53
requireIntegers ();
58
54
59
55
assume ().that (solverToUse ()).isNotEqualTo (Solvers .CVC5 );
@@ -62,17 +58,7 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S
62
58
executor .submit (
63
59
() -> {
64
60
try {
65
- Configuration newConfig =
66
- Configuration .builder ()
67
- .setOption ("solver.solver" , solverToUse ().toString ())
68
- .build ();
69
-
70
- LogManager newLogger = LogManager .createTestLogManager ();
71
- ShutdownNotifier newShutdownNotifier = ShutdownManager .create ().getNotifier ();
72
-
73
- SolverContextFactory newFactory =
74
- new SolverContextFactory (newConfig , newLogger , newShutdownNotifier );
75
- return newFactory .generateContext ();
61
+ return factory .generateContext ();
76
62
} catch (InvalidConfigurationException e ) {
77
63
throw new RuntimeException (e );
78
64
}
@@ -185,7 +171,9 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException
185
171
}
186
172
187
173
@ Override
188
- protected Logics logicToUse () { return Logics .QF_LIA ; }
174
+ protected Logics logicToUse () {
175
+ return Logics .QF_LIA ;
176
+ }
189
177
190
178
// Make sure that the solver returned a valid interpolant for the two formulas
191
179
private void checkInterpolant (
0 commit comments