search

bmoth-mc / bmoth

Model Checker for (a subset of) classical B based on Z3
MIT License
9 stars 1 forks source link

REPL exception for 3>2 #71

Closed leuschel closed 7 years ago

leuschel commented 7 years ago

When I type 3>2 into the REPL, I get:

Exception in thread "JavaFX Application Thread" java.lang.NullPointerException at com.microsoft.z3.Context.checkContextMatch(Context.java:3882) at com.microsoft.z3.Context.mkNot(Context.java:701) at de.bmoth.backend.z3.SolutionFinder.findSolutions(SolutionFinder.java:79) at de.bmoth.app.ReplController.processPredicate(ReplController.java:44) at de.bmoth.app.ReplController.lambda$initialize$0(ReplController.java:33) at com.sun.javafx.event.CompositeEventHandler.dispatchBubblingEvent(CompositeEventHandler.java:86) at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:238) at com.sun.javafx.event.EventHandlerManager.dispatchBubblingEvent(EventHandlerManager.java:191) at com.sun.javafx.event.CompositeEventDispatcher.dispatchBubblingEvent(CompositeEventDispatcher.java:59) at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:58) at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at com.sun.javafx.event.BasicEventDispatcher.dispatchEvent(BasicEventDispatcher.java:56) at com.sun.javafx.event.EventDispatchChainImpl.dispatchEvent(EventDispatchChainImpl.java:114) at com.sun.javafx.event.EventUtil.fireEventImpl(EventUtil.java:74) at com.sun.javafx.event.EventUtil.fireEvent(EventUtil.java:54) at javafx.event.Event.fireEvent(Event.java:198) at javafx.scene.Scene$KeyHandler.process(Scene.java:3964) at javafx.scene.Scene$KeyHandler.access$1800(Scene.java:3910) at javafx.scene.Scene.impl_processKeyEvent(Scene.java:2040) at javafx.scene.Scene$ScenePeerListener.keyEvent(Scene.java:2501) at com.sun.javafx.tk.quantum.GlassViewEventHandler$KeyEventNotification.run(GlassViewEventHandler.java:217) at com.sun.javafx.tk.quantum.GlassViewEventHandler$KeyEventNotification.run(GlassViewEventHandler.java:149) at java.security.AccessController.doPrivileged(Native Method) at com.sun.javafx.tk.quantum.GlassViewEventHandler.lambda$handleKeyEvent$353(GlassViewEventHandler.java:248) at com.sun.javafx.tk.quantum.QuantumToolkit.runWithoutRenderLock(QuantumToolkit.java:389) at com.sun.javafx.tk.quantum.GlassViewEventHandler.handleKeyEvent(GlassViewEventHandler.java:247) at com.sun.glass.ui.View.handleKeyEvent(View.java:546) at com.sun.glass.ui.View.notifyKey(View.java:966)

Building 83% > :run

wysiib commented 7 years ago

The issue is caused by #73

Lunnaris01 commented 7 years ago

now gives "UNSATISFIABLE". We should discuss if we want another output (TRUE/FALSE) for the REPL

wysiib commented 7 years ago

This should not return UNSATISFIABLE. I guess the best would be to report Satisfiable and show the empty model {}.