When trying to edit or create a Constraint when the FeatureModel is void there is an error occurring with the Constraint Dialog.

[oliviia12]

[tthuem]

Thanks for the report.

[jsprey]

An identical but different error also appears when saving a void feature model.
The actuator is also "Creating Empty clause?". Occurs while the configurations are checked and if the model is void.

[jsprey]

Here are the full stack traces for both errors:

Error orccuring when opening constraint dialog:

org.sat4j.specs.ContradictionException: Creating Empty clause ?
	at org.sat4j.minisat.constraints.cnf.Clauses.propagationCheck(Clauses.java:117)
	at org.sat4j.minisat.constraints.cnf.Clauses.sanityCheck(Clauses.java:97)
	at org.sat4j.minisat.constraints.MixedDataStructureDanielWL.createClause(MixedDataStructureDanielWL.java:81)
	at org.sat4j.minisat.core.Solver.addClause(Solver.java:401)
	at org.prop4j.solver.BasicSolver.addClause(BasicSolver.java:134)
	at org.prop4j.solver.BasicSolver.addCNF(BasicSolver.java:122)
	at org.prop4j.solver.BasicSolver.addVariables(BasicSolver.java:94)
	at org.prop4j.solver.BasicSolver.<init>(BasicSolver.java:71)
	at de.ovgu.featureide.fm.ui.editors.ConstraintTextValidator$InitialAnalysis.execute(ConstraintTextValidator.java:142)
	at de.ovgu.featureide.fm.ui.editors.ConstraintTextValidator$InitialAnalysis.execute(ConstraintTextValidator.java:1)
	at de.ovgu.featureide.fm.core.job.Executer.execute(Executer.java:44)
	at de.ovgu.featureide.fm.core.job.LongRunningJob.work(LongRunningJob.java:48)
	at de.ovgu.featureide.fm.core.job.AbstractJob.run(AbstractJob.java:121)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:56)

Error occuring when saving a void feature model:

org.sat4j.specs.ContradictionException: Creating Empty clause ?
	at org.sat4j.minisat.constraints.cnf.Clauses.propagationCheck(Clauses.java:117)
	at org.sat4j.minisat.constraints.cnf.Clauses.sanityCheck(Clauses.java:97)
	at org.sat4j.minisat.constraints.MixedDataStructureDanielWL.createClause(MixedDataStructureDanielWL.java:81)
	at org.sat4j.minisat.core.Solver.addClause(Solver.java:401)
	at org.prop4j.solver.BasicSolver.addClause(BasicSolver.java:134)
	at org.prop4j.solver.BasicSolver.addCNF(BasicSolver.java:122)
	at org.prop4j.solver.BasicSolver.addVariables(BasicSolver.java:94)
	at org.prop4j.solver.BasicSolver.<init>(BasicSolver.java:71)
	at de.ovgu.featureide.core.internal.FeatureProject$7.execute(FeatureProject.java:1089)
	at de.ovgu.featureide.core.internal.FeatureProject$7.execute(FeatureProject.java:1)
	at de.ovgu.featureide.fm.core.job.Executer.execute(Executer.java:44)
	at de.ovgu.featureide.fm.core.job.LongRunningJob.work(LongRunningJob.java:48)
	at de.ovgu.featureide.fm.core.job.AbstractJob.run(AbstractJob.java:121)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:56)

[jsprey]

@skrieter

I created a small examples regarding this problem.

The CNF is as followed:
(Test) & (Test | -Base) & (Base | -Test) & (-Base)

When adding the last clause -Base to the solver it throws a contradiction exception.

Now I catch the ContradictionException and imply that the feature model is void.

Now the error does not longer appear and the constraint editor works as intended.

[jsprey]

Sames goes for the error appearing when checking configurations while the feature model is void.