search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

segmentation fault #248

Closed soonhokong closed 8 years ago

soonhokong commented 8 years ago

Nicola reported:

(set-logic QF_NRA_ODE)
(declare-fun x2 () Real [0.000000, 1.000000])
(declare-fun x1 () Real [0.000000, 1.000000])
(declare-fun vX2 () Int [0.000000, 1.000000])
(declare-fun tau () Real [0.000000, 11.000000])
(declare-fun k2 () Real [0.000000, 1.000000])
(declare-fun k1 () Real [0.000000, 1.000000])
(declare-fun x2_0_0 () Real [0.000000, 1.000000])
(declare-fun x2_0_t () Real [0.000000, 1.000000])
(declare-fun x1_0_0 () Real [0.000000, 1.000000])
(declare-fun x1_0_t () Real [0.000000, 1.000000])
(declare-fun vX2_0_0 () Int [0.000000, 1.000000])
(declare-fun vX2_0_t () Int [0.000000, 1.000000])
(declare-fun tau_0_0 () Real [0.000000, 11.000000])
(declare-fun tau_0_t () Real [0.000000, 11.000000])
(declare-fun k2_0_0 () Real [0.000000, 1.000000])
(declare-fun k2_0_t () Real [0.000000, 1.000000])
(declare-fun k1_0_0 () Real [0.000000, 1.000000])
(declare-fun k1_0_t () Real [0.000000, 1.000000])
(declare-fun time_0 () Real [0.000000, 11.000000])
(declare-fun mode_0 () Real [1.000000, 1.000000])
(define-ode flow_1 (
(= d/dt[k1] 0)
(= d/dt[k2] 0)
(= d/dt[tau] 1)
(= d/dt[vX2] 0)
(= d/dt[x1] (- (* x2 k2) (* (* x1 (^ x2 vX2)) k1)))
(= d/dt[x2] (- (* (* x1 (^ x2 vX2)) k1) (* x2 k2)))))
(assert (and (and (= tau_0_0 0) (= x2_0_0 1) (= x1_0_0 0)) (= mode_0 1) (= vX2_0_t (+ vX2_0_0 (* 0 time_0))) (= tau_0_t (+ tau_0_0 (* 1 time_0))) (= k2_0_t (+ k2_0_0 (* 0 time_0))) (= k1_0_t (+ k1_0_0 (* 0 time_0)))
(= [k1_0_t k2_0_t tau_0_t vX2_0_t x1_0_t x2_0_t] (integral 0. time_0 [k1_0_0 k2_0_0 tau_0_0 vX2_0_0 x1_0_0 x2_0_0] flow_1))
(= mode_0 1) (= mode_0 1) (= tau_0_t 10) (> x1_0_t x2_0_t)))
(check-sat)
(exit)
Exception Type:        EXC_BAD_ACCESS (SIGSEGV)
Exception Codes:       EXC_I386_GPFLT

Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0   dReal                           0x000000010ed035ad std::__1::enable_if<(__is_forward_iterator<std::__1::__wrap_iter<dreal::contractor const*> >::value) && (is_constructible<dreal::contractor, std::__1::iterator_traits<std::__1::__wrap_iter<dreal::contractor const*> >::reference>::value), std::__1::__wrap_iter<dreal::contractor*> >::type std::__1::vector<dreal::contractor, std::__1::allocator<dreal::contractor> >::insert<std::__1::__wrap_iter<dreal::contractor const*> >(std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>) + 15469
1   dReal                           0x000000010ed021e8 std::__1::enable_if<(__is_forward_iterator<std::__1::__wrap_iter<dreal::contractor const*> >::value) && (is_constructible<dreal::contractor, std::__1::iterator_traits<std::__1::__wrap_iter<dreal::contractor const*> >::reference>::value), std::__1::__wrap_iter<dreal::contractor*> >::type std::__1::vector<dreal::contractor, std::__1::allocator<dreal::contractor> >::insert<std::__1::__wrap_iter<dreal::contractor const*> >(std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>) + 10408
2   dReal                           0x000000010ed002c1 std::__1::enable_if<(__is_forward_iterator<std::__1::__wrap_iter<dreal::contractor const*> >::value) && (is_constructible<dreal::contractor, std::__1::iterator_traits<std::__1::__wrap_iter<dreal::contractor const*> >::reference>::value), std::__1::__wrap_iter<dreal::contractor*> >::type std::__1::vector<dreal::contractor, std::__1::allocator<dreal::contractor> >::insert<std::__1::__wrap_iter<dreal::contractor const*> >(std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>, std::__1::__wrap_iter<dreal::contractor const*>) + 2433
3   dReal                           0x000000010ecdb675 nlohmann::basic_json<std::__1::map, std::__1::vector, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, bool, long long, double, std::__1::allocator>& nlohmann::basic_json<std::__1::map, std::__1::vector, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >, bool, long long, double, std::__1::allocator>::operator[]<char, 7ul>(char const (&) [7ul]) + 4453
4   dReal                           0x000000010ec3c453 Enode::isUFOp() const + 17699
5   dReal                           0x000000010ecc5d2d std::__1::vector<bool, std::__1::allocator<bool> >::resize(unsigned long, bool) + 4813
6   dReal                           0x000000010ec7d2fe std::__1::pair<std::__1::__map_iterator<std::__1::__tree_iterator<std::__1::__value_type<Enode*, bool>, std::__1::__tree_node<std::__1::__value_type<Enode*, bool>, void*>*, long> >, bool> std::__1::map<Enode*, bool, std::__1::less<Enode*>, std::__1::allocator<std::__1::pair<Enode* const, bool> > >::emplace<Enode*&, bool&>(Enode*&&&, bool&&&) + 2526
7   dReal                           0x000000010ec6d01c Heap<CoreSMTSolver::VarOrderLt>::remove(int) + 1596
8   dReal                           0x000000010ec6f9df CoreSMTSolver::boolVarDecActivity() + 2271
9   dReal                           0x000000010ec72de9 Heap<SimpSMTSolver::ElimLt>::insert(int) + 2137
10  dReal                           0x000000010ec2d3d5 SMTConfig::setDiagnosticOutputChannel(char const*) + 5381
11  dReal                           0x000000010ec2c3ab SMTConfig::setDiagnosticOutputChannel(char const*) + 1243
12  dReal                           0x000000010ec2c0e3 SMTConfig::setDiagnosticOutputChannel(char const*) + 531
13  dReal                           0x000000010ec1aa26 0x10ec19000 + 6694
14  libdyld.dylib                   0x00007fff959995c9 start + 1
soonhokong commented 8 years ago

It turns out that it's clang-3.8 problem. I've switched back to clang-3.6 to generate pre-compiled binaries on OSX.